diff options
| author | aspiwack | 2007-05-11 17:00:58 +0000 |
|---|---|---|
| committer | aspiwack | 2007-05-11 17:00:58 +0000 |
| commit | 2dbe106c09b60690b87e31e58d505b1f4e05b57f (patch) | |
| tree | 4476a715b796769856e67f6eb5bb6eb60ce6fb57 /toplevel | |
| parent | 95f043a4aa63630de133e667f3da1f48a8f9c4f3 (diff) | |
Processor integers + Print assumption (see coqdev mailing list for the
details).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |