A Coq plugin for non-recursive extraction of dependencies of terms as globally unique kernel names, derived from coq-dpdgraph.
The easiest way to install the plugin is via OPAM:
opam repo add proofengineering-dev http://opam-dev.proofengineering.org
opam install coq-depends
To build the plugin manually, run make in the root directory. Then, to install it, run make install.
(* require and import plugin *)
Require Import Depends.Depends.
(* constants to analyze *)
Require Import List.
(* print dependencies as JSON for constants *)
Depends map filter.
(* write dependencies to file as JSON for constants *)
Depends "deps.json" map filter.
(* show dependencies as JSON for the types of constants *)
TypeDepends map filter.
(* write dependencies to file as JSON for the type of constants *)
TypeDepends "typedeps.json" map filter.
(* show dependencies as JSON of all constants in given modules *)
ModuleDepends Logic List.
(* write dependencies as JSON to file for all constants in given modules *)
ModuleDepends "deps.json" Logic List.