6 files changed, 17 insertions, 11 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 6880383a31..400acc25b6 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1411,11 +1411,10 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
               refresh_universes ~status:Evd.univ_flexible (Some true)
                 env_evar_unf evd evty
             else evd, evty in
-          let (evd, ev) = new_evar_instance sign evd evty ~filter instance in
-          let evk = fst (destEvar evd ev) in
+          let (evd, evk) = new_pure_evar sign evd evty ~filter in
           evsref := (evk,evty,inst,prefer_abstraction)::!evsref;
           fixed := Evar.Set.add evk !fixed;
-          evd, ev
+          evd, mkEvar (evk, instance)
      in
      let evd, rhs' = apply_on_subterm env_rhs evd fixed set_var test c rhs in
      if debug_ho_unification () then
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 348d7c0b2f..79839099f7 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -698,10 +698,9 @@ let make_projectable_subst aliases sigma evi args =
  *)
 
 let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_sign sign filter inst_in_env =
-  let (evd, evar_in_env) = new_evar_instance sign evd ty_t_in_sign ~filter ~src inst_in_env in
+  let (evd, evk) = new_pure_evar sign evd ty_t_in_sign ~filter ~src in
   let t_in_env = whd_evar evd t_in_env in
-  let (evk, _) = destEvar evd evar_in_env in
-  let evd = define_fun env evd None (destEvar evd evar_in_env) t_in_env in
+  let evd = define_fun env evd None (evk, inst_in_env) t_in_env in
   let ctxt = named_context_of_val sign in
   let inst_in_sign = inst_of_vars (Filter.filter_list filter ctxt) in
   let evar_in_sign = mkEvar (evk, inst_in_sign) in
@@ -770,9 +769,9 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
     define_evar_from_virtual_equation define_fun env evd src ty_in_env
       ty_t_in_sign sign2 filter2 inst2_in_env in
   let (evd, ev2_in_sign) =
-    new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 ~src inst2_in_sign in
-  let ev2_in_env = (fst (destEvar evd ev2_in_sign), inst2_in_env) in
-  (evd, ev2_in_sign, ev2_in_env)
+    new_pure_evar sign2 evd ev2ty_in_sign ~filter:filter2 ~src in
+  let ev2_in_env = (ev2_in_sign, inst2_in_env) in
+  (evd, mkEvar (ev2_in_sign, inst2_in_sign), ev2_in_env)
 
 let restrict_upon_filter evd evk p args =
   let oldfullfilter = evar_filter (Evd.find_undefined evd evk) in
diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml
index 05abb86f46..81a62a7048 100644
--- a/pretyping/globEnv.ml
+++ b/pretyping/globEnv.ml
@@ -110,7 +110,8 @@ let new_evar env sigma ?src ?naming typ =
   let instance = rel_list (nb_rel env.renamed_env) inst_vars in
   let (subst, _, sign) = Lazy.force env.extra in
   let typ' = csubst_subst subst typ in
-  new_evar_instance sign sigma typ' ?src ?naming instance
+  let (sigma, evk) = new_pure_evar sign sigma typ' ?src ?naming in
+  (sigma, mkEvar (evk, instance))
 
 let new_type_evar env sigma ~src =
   let sigma, s = Evd.new_sort_variable Evd.univ_flexible_alg sigma in
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index a8e934d3c6..c26da8ccc7 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -185,7 +185,7 @@ let rec cs_pattern_of_constr env t =
   | Rel n -> Default_cs, Some n, []
   | Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b]
   | Proj (p, c) ->
-    let { Environ.uj_type = ty } = Typeops.infer env c in
+    let ty = Retyping.get_type_of_constr env c in
     let _, params = Inductive.find_rectype env ty in
     Const_cs (GlobRef.ConstRef (Projection.constant p)), None, params @ [c]
   | Sort s -> Sort_cs (Sorts.family s), None, []
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index ebf9d4ed1c..4bd22e76cb 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -260,6 +260,9 @@ let get_type_of ?(polyprop=true) ?(lax=false) env sigma c =
 (* Makes an unsafe judgment from a constr *)
 let get_judgment_of env evc c = { uj_val = c; uj_type = get_type_of env evc c }
 
+let get_type_of_constr ?polyprop ?lax env ?(uctx=UState.from_env env) c =
+  EConstr.Unsafe.to_constr (get_type_of ?polyprop ?lax env (Evd.from_ctx uctx) (EConstr.of_constr c))
+
 (* Returns sorts of a context *)
 let sorts_of_context env evc ctxt =
   let rec aux = function
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 16bc251c2a..2e19ffdfcd 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -30,6 +30,10 @@ exception RetypeError of retype_error
 val get_type_of :
   ?polyprop:bool -> ?lax:bool -> env -> evar_map -> constr -> types
 
+(** No-evar version of [get_type_of] *)
+val get_type_of_constr : ?polyprop:bool -> ?lax:bool
+  -> env -> ?uctx:UState.t -> Constr.t -> Constr.types
+
 val get_sort_of :
   ?polyprop:bool -> env -> evar_map -> types -> Sorts.t