Added clenv_environments_evars that behaves as clen_environments but

generating evars in place of metas. Notice that thanks to this changement
unification can be more effective (expecially after reduction) since evars
have non-empty contexts whereas metas have not.


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

2 files changed, 19 insertions, 0 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 4b8ed1ed1..1eccc645d 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -92,6 +92,23 @@ let clenv_environments evd bound c =
   in 
   clrec (evd,[]) bound c
 
+let clenv_environments_evars env evd bound c =
+  let rec clrec (e,ts) n c =
+    match n, kind_of_term c with
+      | (Some 0, _) -> (e, List.rev ts, c)
+      | (n, Cast (c,_)) -> clrec (e,ts) n c
+      | (n, Prod (na,c1,c2)) ->
+          let e',constr = Evarutil.new_evar e env c1 in
+	  let dep = dependent (mkRel 1) c2 in
+	  let na' = if dep then na else Anonymous in
+	  clrec (e', constr::ts) (option_app ((+) (-1)) n)
+	    (if dep then (subst1 constr c2) else c2)
+      | (n, LetIn (na,b,_,c)) ->
+	  clrec (e,ts) (option_app ((+) (-1)) n) (subst1 b c)
+      | (n, _) -> (e, List.rev ts, c)
+  in 
+  clrec (evd,[]) bound c
+
 let mk_clenv_from_n gls n (c,cty) =
   let evd = create_evar_defs gls.sigma in
   let (env,args,concl) = clenv_environments evd n cty in
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index 090b9c661..9ad64e31d 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -108,6 +108,8 @@ val make_clenv_binding :
 (* other stuff *)
 val clenv_environments :
  evar_defs -> int option -> types -> evar_defs * constr list * types
+val clenv_environments_evars :
+ env -> evar_defs -> int option -> types -> evar_defs * constr list * types
 
 (***************************************************************)
 (* Pretty-print *)