diff options
| -rw-r--r-- | kernel/environ.ml | 10 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 2 | ||||
| -rw-r--r-- | parsing/printer.ml | 4 |
3 files changed, 10 insertions, 6 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) diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index f12f730610..668cfe6f30 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -828,7 +828,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 Needed Assumptions"++spc()++pr_reference qid + | PrintNeededAssumptions 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/parsing/printer.ml b/parsing/printer.ml index 307e0af231..97c1f6b7bf 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -486,7 +486,7 @@ let pr_assumptionset env s = str "Section Variables:" ++ fnl () ++ (Environ.AssumptionSet.fold (function Variable (id,typ ) -> fun s -> - str (string_of_identifier id)++str " : "++pr_ltype typ++spc ()++s) + s++str (string_of_identifier id)++str " : "++pr_ltype typ++spc ()) vars (fnl ())) else mt () @@ -494,7 +494,7 @@ let pr_assumptionset env s = if not (Environ.AssumptionSet.is_empty axioms) then str "Axioms:" ++ fnl () ++ (Environ.AssumptionSet.fold - (function Axiom (cst, typ) -> fun s -> (pr_constant env cst)++str " : "++pr_ltype typ++spc ()++s) + (function Axiom (cst, typ) -> fun s -> s++(pr_constant env cst)++str " : "++pr_ltype typ++spc ()) axioms (mt ())) else mt () |