Corrections dans le Print Assumption. Les definitions locales ("Let")

sont maintenant prises en compte (ca a l'air de marcher). En plus j'ai 
corrige l'ordre d'impression pour que ca imprime les noms dans l'ordre 
alphabetique (avant c'etait l'ordre inverse, etonnament perturbant).





git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9873 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 3 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 6835270454..082458fab6 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -543,15 +543,19 @@ 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 simply means that the term refers
-    to a section variable,
+    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
     the constant and return the needed assumptions of its body in the 
     environnement *)
   match kind_of_term t with
-    | Var id -> AssumptionSet.singleton (Variable (id,named_type id env))
+    | 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
     | Cast (e1,_,e2) | Prod (_,e1,e2) | Lambda (_,e1,e2) -> 
                    (needed_assumptions e1 env)**(needed_assumptions e2 env)