Relying on the precomputation of the renaming also for new_evar_type.

4 files changed, 16 insertions, 12 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 668c2770d2..7baa755ab5 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -406,9 +406,14 @@ let coerce_to_indtype typing_fun evdref env matx tomatchl =
 (* Utils *)
 
 let mkExistential env ?(src=(Loc.tag Evar_kinds.InternalHole)) evdref =
-  let (e, u) = evd_comb1 (new_type_evar env  ~src:src) evdref univ_flexible_alg in
+  let (e, u) = evd_comb1 (new_type_evar env ~src:src) evdref univ_flexible_alg in
   e
 
+let evd_comb2 f evdref x y =
+  let (evd',y) = f !evdref x y in
+  evdref := evd';
+  y
+
 let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) =
   (* Ideally, we could find a common inductive type to which both the
      term to match and the patterns coerce *)
diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml
index 57bedf1ee9..12788e5ec5 100644
--- a/pretyping/globEnv.ml
+++ b/pretyping/globEnv.ml
@@ -107,6 +107,11 @@ let e_new_evar env evdref ?src ?naming typ =
   evdref := sigma;
   e
 
+let e_new_type_evar env evdref ~src =
+  let (evd', s) = Evd.new_sort_variable Evd.univ_flexible_alg !evdref in
+  evdref := evd';
+  e_new_evar env evdref ~src (EConstr.mkSort s)
+
 let hide_variable env expansion id =
   let lvar = env.lvar in
   if Id.Map.mem id lvar.ltac_genargs then
diff --git a/pretyping/globEnv.mli b/pretyping/globEnv.mli
index 2d67e25dcd..4038523211 100644
--- a/pretyping/globEnv.mli
+++ b/pretyping/globEnv.mli
@@ -56,6 +56,8 @@ val push_rec_types : evar_map -> Name.t array * constr array -> t -> Name.t arra
 val e_new_evar : t -> evar_map ref -> ?src:Evar_kinds.t Loc.located ->
   ?naming:Namegen.intro_pattern_naming_expr -> constr -> constr
 
+val e_new_type_evar : t -> evar_map ref -> src:Evar_kinds.t Loc.located -> constr
+
 (** [hide_variable env na id] tells to hide the binding of [id] in
     the ltac environment part of [env] and to additionally rebind
     it to [id'] in case [na] is some [Name id']. It is useful e.g.
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 57a259b311..d10c00fa6e 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -454,13 +454,7 @@ let pretype_sort ?loc evdref = function
   | GType s -> evd_comb1 (judge_of_Type ?loc) evdref s
 
 let new_type_evar env evdref loc =
-  let sigma = !evdref in
-  let (sigma, (e, _)) =
-    Evarutil.new_type_evar !!env sigma
-      univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)
-  in
-  evdref := sigma;
-  e
+  e_new_type_evar env evdref ~src:(Loc.tag ?loc Evar_kinds.InternalHole)
 
 (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *)
 (* in environment [env], with existential variables [evdref] and *)
@@ -508,16 +502,14 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) evdref
       let ty =
         match tycon with
         | Some ty -> ty
-        | None ->
-          new_type_evar env evdref loc in
+        | None -> new_type_evar env evdref loc in
         { uj_val = e_new_evar env evdref ~src:(loc,k) ~naming ty; uj_type = ty }
 
   | GHole (k, _naming, Some arg) ->
       let ty =
         match tycon with
         | Some ty -> ty
-        | None ->
-          new_type_evar env evdref loc in
+        | None -> new_type_evar env evdref loc in
       let (c, sigma) = GlobEnv.interp_glob_genarg env !evdref ty arg in
       let () = evdref := sigma in
       { uj_val = c; uj_type = ty }