5 files changed, 9 insertions, 17 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 9bd7ccda5d..db76d08736 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -47,16 +47,6 @@ let clenv_meta_type clenv mv = Typing.meta_type clenv.env clenv.evd mv
 let clenv_value clenv = meta_instance clenv.env clenv.evd clenv.templval
 let clenv_type clenv = meta_instance clenv.env clenv.evd clenv.templtyp
 
-let refresh_undefined_univs clenv =
-  match EConstr.kind clenv.evd clenv.templval.rebus with
-  | Var _ -> clenv, Univ.empty_level_subst
-  | App (f, args) when isVar clenv.evd f -> clenv, Univ.empty_level_subst
-  | _ ->
-    let evd', subst = Evd.refresh_undefined_universes clenv.evd in
-    let map_freelisted f = { f with rebus = subst_univs_level_constr subst f.rebus } in
-      { clenv with evd = evd'; templval = map_freelisted clenv.templval;
-        templtyp = map_freelisted clenv.templtyp }, subst
-
 let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t
 
 let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index fd1e2fe593..43e808dac7 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -45,9 +45,6 @@ val mk_clenv_from_n :
   Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv
 val mk_clenv_from_env : env -> evar_map -> int option -> EConstr.constr * EConstr.types -> clausenv
 
-(** Refresh the universes in a clenv *)
-val refresh_undefined_univs : clausenv -> clausenv * Univ.universe_level_subst
-
 (** {6 linking of clenvs } *)
 
 val clenv_fchain :
diff --git a/proofs/goal.ml b/proofs/goal.ml
index beeaa60433..1c3aed8fc2 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -8,7 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Util
 open Pp
 
 module NamedDecl = Context.Named.Declaration
@@ -58,12 +57,11 @@ module V82 = struct
        goals are restored to their initial value after the evar is
        created. *)
     let prev_future_goals = Evd.save_future_goals evars in
+    let inst = EConstr.identity_subst_val hyps in
     let (evars, evk) =
-      Evarutil.new_pure_evar ~src:(Loc.tag Evar_kinds.GoalEvar) ~typeclass_candidate:false hyps evars concl
+      Evarutil.new_pure_evar ~src:(Loc.tag Evar_kinds.GoalEvar) ~typeclass_candidate:false ~identity:inst hyps evars concl
     in
     let evars = Evd.restore_future_goals evars prev_future_goals in
-    let ctxt = Environ.named_context_of_val hyps in
-    let inst = List.map (NamedDecl.get_id %> EConstr.mkVar) ctxt in
     let ev = EConstr.mkEvar (evk,inst) in
     (evk, ev, evars)
 
diff --git a/proofs/proof.ml b/proofs/proof.ml
index a183fa7797..38fcdd6e5f 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -356,6 +356,10 @@ let compact p =
   let entry, proofview = Proofview.compact p.entry p.proofview in
   { p with proofview; entry }
 
+let update_sigma_env p env =
+  let proofview = Proofview.Unsafe.update_sigma_env p.proofview env in
+  { p with proofview }
+
 (*** Function manipulation proof extra informations ***)
 
 (*** Tactics ***)
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 0e5bdaf07d..2d4966676e 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -78,6 +78,9 @@ val partial_proof : t -> EConstr.constr list
 
 val compact : t -> t
 
+(** [update_sigma_env] lifts [Evd.update_sigma_env] to the proof *)
+val update_sigma_env : t -> Environ.env -> t
+
 (* Returns the proofs (with their type) of the initial goals.
     Raises [UnfinishedProof] is some goals remain to be considered.
     Raises [HasShelvedGoals] if some goals are left on the shelf.