diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 12 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 1 |
2 files changed, 13 insertions, 0 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 433b561c1c..1eb1f89867 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -976,6 +976,18 @@ let vernac_print = function pp (Notation.pr_visibility (Constrextern.without_symbols pr_lrawconstr) s) | PrintAbout qid -> msgnl (print_about qid) | PrintImplicit qid -> msg (print_impargs qid) +(*spiwack: prints all the axioms and section variables used by a term *) + | PrintNeededAssumptions qid -> + let cstr = constr_of_reference (global qid) + in + let nassumptions = Environ.needed_assumptions cstr + (Global.env ()) + in + msg + (try + Printer.pr_assumptionset (Global.env ()) nassumptions + with Not_found -> + pr_reference qid ++ str " is closed under the global context") let global_module r = let (loc,qid) = qualid_of_reference r in diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 5c1b138550..9714ffd6c9 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -64,6 +64,7 @@ type printable = | PrintVisibility of string option | PrintAbout of reference | PrintImplicit of reference + | PrintNeededAssumptions of reference type search_about_item = | SearchRef of reference |