More unification in type_of and addition of e_type_of to get the new

evar_map after instantiations possibly happened.

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

2 files changed, 14 insertions, 0 deletions

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index ebd099fa3..7f84828f1 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -45,6 +45,11 @@ let e_judge_of_apply env evdref funj argjv =
 	   apply_rec (n+1) (subst1 hj.uj_val c2) restjl
 	 else
 	   error_cant_apply_bad_type env (n,c1, hj.uj_type) funj argjv
+      | Evar ev ->
+	  let (evd',t) = Evarutil.define_evar_as_product !evdref ev in
+          evdref := evd';
+          let (_,_,c2) = destProd t in
+	  apply_rec (n+1) (subst1 hj.uj_val c2) restjl
       | _ ->
 	  error_cant_apply_not_functional env funj argjv
   in
@@ -261,6 +266,12 @@ let sort_of env evd c =
 
 (* Try to solve the existential variables by typing *)
 
+let e_type_of env evd c =
+  let evdref = ref evd in
+  let j = execute env evdref c in
+  (* side-effect on evdref *)
+  !evdref, Termops.refresh_universes j.uj_type
+
 let solve_evars env evd c =
   let evdref = ref evd in
   let c = (execute env evdref c).uj_val in
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 2c9a6c6c0..224fd995a 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -17,6 +17,9 @@ open Evd
 (** Typecheck a term and return its type *)
 val type_of : env -> evar_map -> constr -> types
 
+(** Typecheck a term and return its type + updated evars *)
+val e_type_of : env -> evar_map -> constr -> evar_map * types
+
 (** Typecheck a type and return its sort *)
 val sort_of : env -> evar_map -> types -> sorts