aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
authorGravatar aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-11-09 17:37:11 +0000
committerGravatar aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-11-09 17:37:11 +0000
commita2c53cc24077ec911877d9c12e22819b27c516c8 (patch)
treef68db29a55b0617703e8cfda523d76c37a8ef58d /toplevel
parent471df7db322e77a3cb66a8def53c7ddfdb9c8769 (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.ml4
-rw-r--r--toplevel/vernacexpr.ml2
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