diff options
author | 2007-11-09 17:37:11 +0000 | |
---|---|---|
committer | 2007-11-09 17:37:11 +0000 | |
commit | a2c53cc24077ec911877d9c12e22819b27c516c8 (patch) | |
tree | f68db29a55b0617703e8cfda523d76c37a8ef58d /toplevel | |
parent | 471df7db322e77a3cb66a8def53c7ddfdb9c8769 (diff) |
Nettoyage de Print Assumptions :
- Le code est maintenant mieux commenté.
- J'ai aussi réorganisé un petit peu pour le rendre plus léger, mais
presque rien
- j'ai changé les noms internes : needed_assumptions devient
assumptions et PrintNeededAssumptions devient PrintAssumptions
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10311 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/vernacentries.ml | 4 | ||||
-rw-r--r-- | toplevel/vernacexpr.ml | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 784cabcd5..d6b874c22 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -967,9 +967,9 @@ let vernac_print = function | 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 r -> + | PrintAssumptions r -> let cstr = constr_of_global (global_with_alias r) in - let nassumptions = Environ.needed_assumptions cstr (Global.env ()) in + let nassumptions = Environ.assumptions cstr (Global.env ()) in msg (try Printer.pr_assumptionset (Global.env ()) nassumptions diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index c1a8625bc..c89393301 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -64,7 +64,7 @@ type printable = | PrintVisibility of string option | PrintAbout of reference | PrintImplicit of reference - | PrintNeededAssumptions of reference + | PrintAssumptions of reference type search_about_item = | SearchRef of reference |