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

8 files changed, 51 insertions, 42 deletions

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 4f98b7396b..150b070f88 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1832,7 +1832,7 @@ let rec xlate_vernac =
 	    CT_print_path (xlate_class id1, xlate_class id2)
 	| PrintCanonicalConversions ->
 	    xlate_error "TODO: Print Canonical Structures"
-	| PrintNeededAssumptions _ -> 
+	| PrintAssumptions _ -> 
 	    xlate_error "TODO: Print Needed Assumptions"
 	| PrintInspect n -> CT_inspect (CT_int n)
 	| PrintUniverses opt_s -> CT_print_universes(ctf_STRING_OPT opt_s)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 4266602983..faf0757127 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -528,14 +528,18 @@ fun env field value ->
   }
 
 
+(**************************************************************)
 (* spiwack: the following definitions are used by the function 
-   needed_assumption which gives as an output the set of all
+   [assumptions] which gives as an output the set of all
    axioms and sections variables on which a given term depends
    in a context (expectingly the Global context) *)
+
 type assumption =
-  | Variable of identifier*constr
-  | Axiom of constant*constr
+  | Variable of identifier*constr (* A section variable and its type *)
+  | Axiom of constant*constr      (* An axiom and its type*)
+
 
+(* Defines a set of [assumption] *)
 module OrderedAssumption = 
 struct 
   type t = assumption
@@ -544,45 +548,43 @@ end
 
 module AssumptionSet = Set.Make (OrderedAssumption)
 
-(* definition for redability purposes *)
+(* infix definition of set-union for redability purposes *)
 let ( ** ) s1 s2  = AssumptionSet.union s1 s2
 
-let rec needed_assumptions t env =   
- (* goes recursively into the terms to see if it depends on assumptions
-    the 3 important cases are : Var _ which means that the term refers
-    to a section variable or a "Let" definition,
-                                Rel _ which means the term is a variable
-    which has been bound earlier by a Lambda or a Prod (returns [] )
-                                Const _ where we need to first unfold
+let rec assumptions t env =   
+ (* Goes recursively into the terms to see if it depends on assumptions
+    the 3 important cases are : - Const _ where we need to first unfold
     the constant and return the needed assumptions of its body in the 
-    environnement *)
+    environment,
+                                - Rel _ which means the term is a variable
+    which has been bound earlier by a Lambda or a Prod (returns [] ),
+                                - Var _ which means that the term refers
+    to a section variable or a "Let" definition, in the former it is
+    an assumption of [t], in the latter is must be unfolded like a Const.
+    The other cases are straightforward recursion.*)
   match kind_of_term t with
-    | Var id -> (* a var can be either a variable, or a "Let" definition.*)
+    | Var id -> (* a Var can be either a variable, or a "Let" definition.*)
                 (match named_body id env with
                 | None ->
                       AssumptionSet.singleton (Variable (id,named_type id env))
-		| Some bdy -> needed_assumptions bdy env)
-    | Meta _ | Evar _ -> assert false
+		| Some bdy -> assumptions bdy env)
+    | Meta _ | Evar _ -> Util.anomaly "Environ.assumption: does not expect a meta or an evar"
     | Cast (e1,_,e2) | Prod (_,e1,e2) | Lambda (_,e1,e2) -> 
-                   (needed_assumptions e1 env)**(needed_assumptions e2 env)
-    | LetIn (_,e1,e2,e3) ->(needed_assumptions e1 env)**
-                           (needed_assumptions e2 env)**
-                           (needed_assumptions e3 env)
-    | App (e1, e_array) -> (needed_assumptions e1 env)**
-                   (Array.fold_right (fun e -> fun s -> 
-                                               (needed_assumptions e env)**s)
+                   (assumptions e1 env)**(assumptions e2 env)
+    | LetIn (_,e1,e2,e3) ->(assumptions e1 env)**
+                           (assumptions e2 env)**
+                           (assumptions e3 env)
+    | App (e1, e_array) -> (assumptions e1 env)**
+                   (Array.fold_right (fun e s -> (assumptions e env)**s)
                                       e_array AssumptionSet.empty)
-    | Case (_,e1,e2,e_array) -> (needed_assumptions e1 env)**
-                                (needed_assumptions e2 env)**
-                   (Array.fold_right (fun e -> fun s -> 
-                                               (needed_assumptions e env)**s)
+    | Case (_,e1,e2,e_array) -> (assumptions e1 env)**
+                                (assumptions e2 env)**
+                   (Array.fold_right (fun e s -> (assumptions e env)**s)
                                       e_array AssumptionSet.empty)
     | Fix (_,(_, e1_array, e2_array)) | CoFix (_,(_,e1_array, e2_array)) ->
-                   Array.fold_right (fun e -> fun s -> 
-                                              (needed_assumptions e env)**s)
+                   Array.fold_right (fun e s -> (assumptions e env)**s)
                                       e1_array
-                   (Array.fold_right (fun e -> fun s -> 
-                                              (needed_assumptions e env)**s)
+                   (Array.fold_right (fun e s -> (assumptions e env)**s)
                                       e2_array AssumptionSet.empty)
     | Const kn -> 
 	let cb = lookup_constant kn env in
@@ -594,7 +596,7 @@ let rec needed_assumptions t env =
 		| NonPolymorphicType t -> t
 	    in
 	    AssumptionSet.singleton (Axiom (kn,ctype))
-        | Some body -> needed_assumptions (Declarations.force body) env)
+        | Some body -> assumptions (Declarations.force body) env)
     | _ -> AssumptionSet.empty (* closed atomic types + rel *)
 
 (* /spiwack *)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 293c55a691..bfbb5dd3c2 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -231,15 +231,22 @@ val unregister : env -> field -> env
 
 val register : env -> field -> Retroknowledge.entry -> env
 
+
+
+(******************************************************************)
 (* spiwack: a few declarations for the "Print Assumption" command *)
+
 type assumption =
-  | Variable of identifier*Term.constr
-  | Axiom of constant*Term.constr
+  | Variable of identifier*Term.constr (* A section variable and its type *)
+  | Axiom of constant*Term.constr      (* An axiom and its type*)
 
-module OrderedAssumption :  Set.OrderedType with type t = assumption
 
+(* AssumptionSet.t is a set of [assumption] *)
+module OrderedAssumption :  Set.OrderedType with type t = assumption
 module AssumptionSet : Set.S with type elt = assumption
 
-val needed_assumptions : constr -> env -> AssumptionSet.t
+(* collects all the assumptions on which a term relies (together with
+   their type *)
+val assumptions : constr -> env -> AssumptionSet.t
 
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index d65caf7cab..91e4c73fc9 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -109,7 +109,7 @@ let env_of_senv = env_of_safe_env
 (* terms which are closed under the environnement env, i.e
    terms which only depends on constant who are themselves closed *)
 let closed env term = 
-  AssumptionSet.is_empty (needed_assumptions env term)
+  AssumptionSet.is_empty (assumptions env term)
 
 (* the set of safe terms in an environement any recursive set of
    terms who are known not to prove inconsistent statement. It should
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index b7cde536f7..a64cf74cc7 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -634,7 +634,7 @@ GEXTEND Gram
       | IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s
       | IDENT "Implicit"; qid = global -> PrintImplicit qid
       | IDENT "Universes"; fopt = OPT ne_string -> PrintUniverses fopt
-      | IDENT "Assumptions"; qid = global -> PrintNeededAssumptions qid ] ]
+      | IDENT "Assumptions"; qid = global -> PrintAssumptions qid ] ]
   ;
   class_rawexpr:
     [ [ IDENT "Funclass" -> FunClass
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 4bb7d27520..a5bcea6f1b 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -834,7 +834,7 @@ let rec pr_vernac = function
 	| PrintImplicit qid -> str"Print Implicit" ++ spc()  ++ pr_reference qid
 (* spiwack: command printing all the axioms and section variables used in a 
          term *)
-	| PrintNeededAssumptions qid -> str"Print Assumptions"++spc()++pr_reference qid
+	| PrintAssumptions qid -> str"Print Assumptions"++spc()++pr_reference qid
       in pr_printable p
   | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_pattern_expr
   | VernacLocate loc -> 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 784cabcd5c..d6b874c228 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 c1a8625bce..c893933015 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