1 files changed, 315 insertions, 182 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index c570f75c6b..4ae1d034d7 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -139,6 +139,29 @@ module Abstraction = struct
   let abstract_last l = Abstract :: l
 end
 
+module Identity :
+sig
+  type t
+  val make : econstr list -> t
+  val none : unit -> t
+  val repr : named_context_val -> Filter.t -> t -> econstr list
+  val is_identity : econstr list -> t -> bool
+end =
+struct
+  type t = econstr list option ref
+  let make s = ref (Some s)
+  let none () = ref None
+  let repr sign filter s = match !s with
+  | None ->
+    let ans = Filter.filter_list filter sign.env_named_var in
+    let () = s := Some ans in
+    ans
+  | Some s -> s
+  let is_identity l s = match !s with
+  | None -> false
+  | Some s -> s == l
+end
+
 (* The kinds of existential variables are now defined in [Evar_kinds] *)
 
 (* The type of mappings for existential variables *)
@@ -158,7 +181,9 @@ type evar_info = {
   evar_filter : Filter.t;
   evar_abstract_arguments : Abstraction.t;
   evar_source : Evar_kinds.t Loc.located;
-  evar_candidates : constr list option; (* if not None, list of allowed instances *)}
+  evar_candidates : constr list option; (* if not None, list of allowed instances *)
+  evar_identity : Identity.t;
+}
 
 let make_evar hyps ccl = {
   evar_concl = ccl;
@@ -167,7 +192,9 @@ let make_evar hyps ccl = {
   evar_filter = Filter.identity;
   evar_abstract_arguments = Abstraction.identity;
   evar_source = Loc.tag @@ Evar_kinds.InternalHole;
-  evar_candidates = None; }
+  evar_candidates = None;
+  evar_identity = Identity.none ();
+}
 
 let instance_mismatch () =
   anomaly (Pp.str "Signature and its instance do not match.")
@@ -216,6 +243,9 @@ let evar_filtered_env env evi = match Filter.repr (evar_filter evi) with
   in
   make_env filter (evar_context evi)
 
+let evar_identity_subst evi =
+  Identity.repr evi.evar_hyps evi.evar_filter evi.evar_identity
+
 let map_evar_body f = function
   | Evar_empty -> Evar_empty
   | Evar_defined d -> Evar_defined (f d)
@@ -256,7 +286,9 @@ let evar_instance_array test_id info args =
     instrec filter (evar_context info) args
 
 let make_evar_instance_array info args =
-  evar_instance_array (NamedDecl.get_id %> isVarId) info args
+  if Identity.is_identity args info.evar_identity then []
+  else
+    evar_instance_array (NamedDecl.get_id %> isVarId) info args
 
 let instantiate_evar_array info c args =
   let inst = make_evar_instance_array info args in
@@ -419,11 +451,9 @@ let key id (_, idtoev) =
 
 end
 
-type goal_kind = ToShelve | ToGiveUp
-
 type evar_flags =
   { obligation_evars : Evar.Set.t;
-    restricted_evars : Evar.t Evar.Map.t;
+    aliased_evars : Evar.t Evar.Map.t;
     typeclass_evars : Evar.Set.t }
 
 type side_effect_role =
@@ -434,6 +464,124 @@ type side_effects = {
   seff_roles : side_effect_role Cmap.t;
 }
 
+module FutureGoals : sig
+
+  type t = private {
+    comb : Evar.t list;
+    principal : Evar.t option; (** if [Some e], [e] must be
+                                   contained in
+                                   [comb]. The evar
+                                   [e] will inherit
+                                   properties (now: the
+                                   name) of the evar which
+                                   will be instantiated with
+                                   a term containing [e]. *)
+  }
+
+  val map_filter : (Evar.t -> Evar.t option) -> t -> t
+  (** Applies a function on the future goals *)
+
+  val filter : (Evar.t -> bool) -> t -> t
+  (** Applies a filter on the future goals *)
+
+  type stack
+
+  val empty_stack : stack
+
+  val push : stack -> stack
+  val pop : stack -> t * stack
+
+  val add : principal:bool -> Evar.t -> stack -> stack
+  val remove : Evar.t -> stack -> stack
+
+  val fold : ('a -> Evar.t -> 'a) -> 'a -> stack -> 'a
+
+  val pr_stack : stack -> Pp.t
+
+end = struct
+
+  type t = {
+    comb : Evar.t list;
+    principal : Evar.t option; (** if [Some e], [e] must be
+                                   contained in
+                                   [comb]. The evar
+                                   [e] will inherit
+                                   properties (now: the
+                                   name) of the evar which
+                                   will be instantiated with
+                                   a term containing [e]. *)
+  }
+
+  type stack = t list
+
+  let set f = function
+  | [] -> anomaly Pp.(str"future_goals stack should not be empty")
+  | hd :: tl ->
+    f hd :: tl
+
+  let add ~principal evk stack =
+    let add fgl =
+      let comb = evk :: fgl.comb in
+      let principal =
+        if principal then
+          match fgl.principal with
+          | Some _ -> CErrors.user_err Pp.(str "Only one main subgoal per instantiation.")
+          | None -> Some evk
+        else fgl.principal
+      in
+      { comb; principal }
+    in
+    set add stack
+
+  let remove e stack =
+    let remove fgl =
+      let filter e' = not (Evar.equal e e') in
+      let principal = Option.filter filter fgl.principal in
+      let comb = List.filter filter fgl.comb in
+      { principal; comb }
+    in
+    List.map remove stack
+
+  let empty = {
+    principal = None;
+    comb = [];
+  }
+
+  let empty_stack = [empty]
+
+  let push stack = empty :: stack
+
+  let pop stack =
+    match stack with
+    | [] -> anomaly Pp.(str"future_goals stack should not be empty")
+    | hd :: tl ->
+      hd, tl
+
+  let fold f acc stack =
+    let future_goals = List.hd stack in
+    List.fold_left f acc future_goals.comb
+
+  let filter f fgl =
+    let comb = List.filter f fgl.comb in
+    let principal = Option.filter f fgl.principal in
+    { comb; principal }
+
+  let map_filter f fgl =
+    let comb = List.map_filter f fgl.comb in
+    let principal = Option.bind fgl.principal f in
+    { comb; principal }
+
+  let pr_stack stack =
+    let open Pp in
+    let pr_future_goals fgl =
+      prlist_with_sep spc Evar.print fgl.comb ++
+        pr_opt (fun ev -> str"(principal: " ++ Evar.print ev ++ str")") fgl.principal
+    in
+    if List.is_empty stack then str"(empty stack)"
+    else prlist_with_sep (fun () -> str"||") pr_future_goals stack
+
+end
+
 type evar_map = {
   (* Existential variables *)
   defn_evars : evar_info EvMap.t;
@@ -449,17 +597,10 @@ type evar_map = {
   evar_flags : evar_flags;
   (** Interactive proofs *)
   effects    : side_effects;
-  future_goals : Evar.t list; (** list of newly created evars, to be
-                                  eventually turned into goals if not solved.*)
-  principal_future_goal : Evar.t option; (** if [Some e], [e] must be
-                                             contained
-                                             [future_goals]. The evar
-                                             [e] will inherit
-                                             properties (now: the
-                                             name) of the evar which
-                                             will be instantiated with
-                                             a term containing [e]. *)
-  future_goals_status : goal_kind EvMap.t;
+  future_goals : FutureGoals.stack; (** list of newly created evars, to be
+                                        eventually turned into goals if not solved.*)
+  given_up : Evar.Set.t;
+  shelf : Evar.t list list;
   extras : Store.t;
 }
 
@@ -490,7 +631,7 @@ let add_with_name ?name ?(typeclass_candidate = true) d e i = match i.evar_body
     associated to an evar, so we prevent registering its typeclass status. *)
 let add d e i = add_with_name ~typeclass_candidate:false d e i
 
-(*** Evar flags: typeclasses, restricted or obligation flag *)
+(*** Evar flags: typeclasses, aliased or obligation flag *)
 
 let get_typeclass_evars evd = evd.evar_flags.typeclass_evars
 
@@ -518,29 +659,28 @@ let is_obligation_evar evd evk =
 let inherit_evar_flags evar_flags evk evk' =
   let evk_typeclass = Evar.Set.mem evk evar_flags.typeclass_evars in
   let evk_obligation = Evar.Set.mem evk evar_flags.obligation_evars in
-  if not (evk_obligation || evk_typeclass) then evar_flags
-  else
-    let typeclass_evars =
-      if evk_typeclass then
-        let typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars in
-        Evar.Set.add evk' typeclass_evars
-      else evar_flags.typeclass_evars
-    in
-    let obligation_evars =
-      if evk_obligation then
-        let obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars in
-        Evar.Set.add evk' obligation_evars
-      else evar_flags.obligation_evars
-    in
-    { evar_flags with obligation_evars; typeclass_evars }
+  let aliased_evars = Evar.Map.add evk evk' evar_flags.aliased_evars in
+  let typeclass_evars =
+    if evk_typeclass then
+      let typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars in
+      Evar.Set.add evk' typeclass_evars
+    else evar_flags.typeclass_evars
+  in
+  let obligation_evars =
+    if evk_obligation then
+      let obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars in
+      Evar.Set.add evk' obligation_evars
+    else evar_flags.obligation_evars
+  in
+  { obligation_evars; aliased_evars; typeclass_evars }
 
 (** Removal: in all other cases of definition *)
 
 let remove_evar_flags evk evar_flags =
   { typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars;
     obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars;
-    (* Restriction information is kept. *)
-    restricted_evars = evar_flags.restricted_evars }
+    (* Aliasing information is kept. *)
+    aliased_evars = evar_flags.aliased_evars }
 
 (** New evars *)
 
@@ -558,14 +698,9 @@ let new_evar evd ?name ?typeclass_candidate evi =
 let remove d e =
   let undf_evars = EvMap.remove e d.undf_evars in
   let defn_evars = EvMap.remove e d.defn_evars in
-  let principal_future_goal = match d.principal_future_goal with
-  | None -> None
-  | Some e' -> if Evar.equal e e' then None else d.principal_future_goal
-  in
-  let future_goals = List.filter (fun e' -> not (Evar.equal e e')) d.future_goals in
-  let future_goals_status = EvMap.remove e d.future_goals_status in
+  let future_goals = FutureGoals.remove e d.future_goals in
   let evar_flags = remove_evar_flags e d.evar_flags in
-  { d with undf_evars; defn_evars; principal_future_goal; future_goals; future_goals_status;
+  { d with undf_evars; defn_evars; future_goals;
            evar_flags }
 
 let find d e =
@@ -673,7 +808,7 @@ let create_evar_defs sigma = { sigma with
 
 let empty_evar_flags =
   { obligation_evars = Evar.Set.empty;
-    restricted_evars = Evar.Map.empty;
+    aliased_evars = Evar.Map.empty;
     typeclass_evars = Evar.Set.empty }
 
 let empty_side_effects = {
@@ -691,9 +826,9 @@ let empty = {
   metas      = Metamap.empty;
   effects    = empty_side_effects;
   evar_names = EvNames.empty; (* id<->key for undefined evars *)
-  future_goals = [];
-  principal_future_goal = None;
-  future_goals_status = EvMap.empty;
+  future_goals = FutureGoals.empty_stack;
+  given_up = Evar.Set.empty;
+  shelf = [[]];
   extras = Store.empty;
 }
 
@@ -703,6 +838,10 @@ let from_ctx ctx = { empty with universes = ctx }
 
 let has_undefined evd = not (EvMap.is_empty evd.undf_evars)
 
+let has_given_up evd = not (Evar.Set.is_empty evd.given_up)
+
+let has_shelved evd = not (List.for_all List.is_empty evd.shelf)
+
 let evars_reset_evd ?(with_conv_pbs=false) ?(with_univs=true) evd d =
   let conv_pbs = if with_conv_pbs then evd.conv_pbs else d.conv_pbs in
   let last_mods = if with_conv_pbs then evd.last_mods else d.last_mods in
@@ -732,70 +871,12 @@ let evar_source evk d = (find d evk).evar_source
 let evar_ident evk evd = EvNames.ident evk evd.evar_names
 let evar_key id evd = EvNames.key id evd.evar_names
 
-let define_aux def undef evk body =
-  let oldinfo =
-    try EvMap.find evk undef
-    with Not_found ->
-      if EvMap.mem evk def then
-        anomaly ~label:"Evd.define" (Pp.str "cannot define an evar twice.")
-      else
-        anomaly ~label:"Evd.define" (Pp.str "cannot define undeclared evar.")
-  in
-  let () = assert (oldinfo.evar_body == Evar_empty) in
-  let newinfo = { oldinfo with evar_body = Evar_defined body } in
-  EvMap.add evk newinfo def, EvMap.remove evk undef
-
-(* define the existential of section path sp as the constr body *)
-let define_gen evk body evd evar_flags =
-  let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
-  let last_mods = match evd.conv_pbs with
-  | [] ->  evd.last_mods
-  | _ -> Evar.Set.add evk evd.last_mods
-  in
-  let evar_names = EvNames.remove_name_defined evk evd.evar_names in
-  { evd with defn_evars; undf_evars; last_mods; evar_names; evar_flags }
+let get_aliased_evars evd = evd.evar_flags.aliased_evars
 
-(** By default, the obligation and evar tag of the evar is removed *)
-let define evk body evd =
-  let evar_flags = remove_evar_flags evk evd.evar_flags in
-  define_gen evk body evd evar_flags
-
-(** In case of an evar-evar solution, the flags are inherited *)
-let define_with_evar evk body evd =
-  let evk' = fst (destEvar body) in
-  let evar_flags = inherit_evar_flags evd.evar_flags evk evk' in
-  define_gen evk body evd evar_flags
-
-let is_restricted_evar evd evk =
-  try Some (Evar.Map.find evk evd.evar_flags.restricted_evars)
+let is_aliased_evar evd evk =
+  try Some (Evar.Map.find evk evd.evar_flags.aliased_evars)
   with Not_found -> None
 
-let declare_restricted_evar evar_flags evk evk' =
-  { evar_flags with restricted_evars = Evar.Map.add evk evk' evar_flags.restricted_evars }
-
-(* In case of restriction, we declare the restriction and inherit the obligation
-   and typeclass flags. *)
-
-let restrict evk filter ?candidates ?src evd =
-  let evk' = new_untyped_evar () in
-  let evar_info = EvMap.find evk evd.undf_evars in
-  let evar_info' =
-    { evar_info with evar_filter = filter;
-      evar_candidates = candidates;
-      evar_source = (match src with None -> evar_info.evar_source | Some src -> src) } in
-  let last_mods = match evd.conv_pbs with
-  | [] ->  evd.last_mods
-  | _ -> Evar.Set.add evk evd.last_mods in
-  let evar_names = EvNames.reassign_name_defined evk evk' evd.evar_names in
-  let ctxt = Filter.filter_list filter (evar_context evar_info) in
-  let id_inst = List.map (NamedDecl.get_id %> mkVar) ctxt in
-  let body = mkEvar(evk',id_inst) in
-  let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
-  let evar_flags = declare_restricted_evar evd.evar_flags evk evk' in
-  let evar_flags = inherit_evar_flags evar_flags evk evk' in
-  { evd with undf_evars = EvMap.add evk' evar_info' undf_evars;
-    defn_evars; last_mods; evar_names; evar_flags }, evk'
-
 let downcast evk ccl evd =
   let evar_info = EvMap.find evk evd.undf_evars in
   let evar_info' = { evar_info with evar_concl = ccl } in
@@ -987,11 +1068,6 @@ let check_constraints evd csts =
 let fix_undefined_variables evd =
   { evd with universes = UState.fix_undefined_variables evd.universes }
 
-let refresh_undefined_universes evd =
-  let uctx', subst = UState.refresh_undefined_univ_variables evd.universes in
-  let evd' = cmap (subst_univs_level_constr subst) {evd with universes = uctx'} in
-    evd', subst
-
 let nf_univ_variables evd =
   let subst, uctx' = UState.normalize_variables evd.universes in
   let evd' = {evd with universes = uctx'} in
@@ -1008,8 +1084,8 @@ let universe_binders evd = UState.universe_binders evd.universes
 
 let universes evd = UState.ugraph evd.universes
 
-let update_sigma_env evd env =
-  { evd with universes = UState.update_sigma_env evd.universes env }
+let update_sigma_univs ugraph evd =
+  { evd with universes = UState.update_sigma_univs evd.universes ugraph }
 
 exception UniversesDiffer = UState.UniversesDiffer
 
@@ -1031,72 +1107,129 @@ let drop_side_effects evd =
 let eval_side_effects evd = evd.effects
 
 (* Future goals *)
-let declare_future_goal ?tag evk evd =
-  { evd with future_goals = evk::evd.future_goals;
-             future_goals_status = Option.fold_right (EvMap.add evk) tag evd.future_goals_status }
-
-let declare_principal_goal ?tag evk evd =
-  match evd.principal_future_goal with
-  | None -> { evd with
-    future_goals = evk::evd.future_goals;
-    principal_future_goal=Some evk;
-    future_goals_status = Option.fold_right (EvMap.add evk) tag evd.future_goals_status;
-    }
-  | Some _ -> CErrors.user_err Pp.(str "Only one main subgoal per instantiation.")
-
-type future_goals = Evar.t list * Evar.t option * goal_kind EvMap.t
-
-let future_goals evd = evd.future_goals
-
-let principal_future_goal evd = evd.principal_future_goal
-
-let save_future_goals evd =
-  (evd.future_goals, evd.principal_future_goal, evd.future_goals_status)
-
-let reset_future_goals evd =
-  { evd with future_goals = [] ; principal_future_goal = None;
-             future_goals_status = EvMap.empty }
-
-let restore_future_goals evd (gls,pgl,map) =
-  { evd with future_goals = gls ; principal_future_goal = pgl;
-             future_goals_status = map }
-
-let fold_future_goals f sigma (gls,pgl,map) =
-  List.fold_left f sigma gls
-
-let map_filter_future_goals f (gls,pgl,map) =
-  (* Note: map is now a superset of filtered evs, but its size should
-    not be too big, so that's probably ok not to update it *)
-  (List.map_filter f gls,Option.bind pgl f,map)
-
-let filter_future_goals f (gls,pgl,map) =
-  (List.filter f gls,Option.bind pgl (fun a -> if f a then Some a else None),map)
-
-let dispatch_future_goals_gen distinguish_shelf (gls,pgl,map) =
-  let rec aux (comb,shelf,givenup as acc) = function
-    | [] -> acc
-    | evk :: gls ->
-       let acc =
-        try match EvMap.find evk map with
-        | ToGiveUp -> (comb,shelf,evk::givenup)
-        | ToShelve ->
-           if distinguish_shelf then (comb,evk::shelf,givenup)
-           else raise Not_found
-        with Not_found -> (evk::comb,shelf,givenup) in
-       aux acc gls in
-  (* Note: this reverses the order of initial list on purpose *)
-  let (comb,shelf,givenup) = aux ([],[],[]) gls in
-  (comb,shelf,givenup,pgl)
-
-let dispatch_future_goals =
-  dispatch_future_goals_gen true
-
-let extract_given_up_future_goals goals =
-  let (comb,_,givenup,_) = dispatch_future_goals_gen false goals in
-  (comb,givenup)
-
-let shelve_on_future_goals shelved (gls,pgl,map) =
-  (shelved @ gls, pgl, List.fold_right (fun evk -> EvMap.add evk ToShelve) shelved map)
+let declare_future_goal evk evd =
+  let future_goals = FutureGoals.add ~principal:false evk evd.future_goals in
+  { evd with future_goals }
+
+let declare_principal_goal evk evd =
+  let future_goals = FutureGoals.add ~principal:true evk evd.future_goals in
+  { evd with future_goals }
+
+let push_future_goals evd =
+  { evd with future_goals = FutureGoals.push evd.future_goals }
+
+let pop_future_goals evd =
+  let hd, future_goals = FutureGoals.pop evd.future_goals in
+  hd, { evd with future_goals }
+
+let fold_future_goals f sigma =
+  FutureGoals.fold f sigma sigma.future_goals
+
+let remove_future_goal evd evk =
+  { evd with future_goals = FutureGoals.remove evk evd.future_goals }
+
+let pr_future_goals_stack evd =
+  FutureGoals.pr_stack evd.future_goals
+
+let give_up ev evd =
+  { evd with given_up = Evar.Set.add ev evd.given_up }
+
+let push_shelf evd =
+  { evd with shelf = [] :: evd.shelf }
+
+let pop_shelf evd =
+  match evd.shelf with
+  | [] -> anomaly Pp.(str"shelf stack should not be empty")
+  | hd :: tl ->
+    hd, { evd with shelf = tl }
+
+let filter_shelf f evd =
+  { evd with shelf = List.map (List.filter f) evd.shelf }
+
+let shelve evd l =
+  match evd.shelf with
+  | [] -> anomaly Pp.(str"shelf stack should not be empty")
+  | hd :: tl ->
+    { evd with shelf = (hd@l) :: tl }
+
+let unshelve evd l =
+  { evd with shelf = List.map (List.filter (fun ev -> not (CList.mem_f Evar.equal ev l))) evd.shelf }
+
+let given_up evd = evd.given_up
+
+let shelf evd = List.flatten evd.shelf
+
+let pr_shelf evd =
+  let open Pp in
+  if List.is_empty evd.shelf then str"(empty stack)"
+  else prlist_with_sep (fun () -> str"||") (prlist_with_sep spc Evar.print) evd.shelf
+
+let define_aux def undef evk body =
+  let oldinfo =
+    try EvMap.find evk undef
+    with Not_found ->
+      if EvMap.mem evk def then
+        anomaly ~label:"Evd.define" (Pp.str "cannot define an evar twice.")
+      else
+        anomaly ~label:"Evd.define" (Pp.str "cannot define undeclared evar.")
+  in
+  let () = assert (oldinfo.evar_body == Evar_empty) in
+  let newinfo = { oldinfo with evar_body = Evar_defined body } in
+  EvMap.add evk newinfo def, EvMap.remove evk undef
+
+(* define the existential of section path sp as the constr body *)
+let define_gen evk body evd evar_flags =
+  let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
+  let last_mods = match evd.conv_pbs with
+  | [] ->  evd.last_mods
+  | _ -> Evar.Set.add evk evd.last_mods
+  in
+  let evar_names = EvNames.remove_name_defined evk evd.evar_names in
+  { evd with defn_evars; undf_evars; last_mods; evar_names; evar_flags }
+
+(** By default, the obligation and evar tag of the evar is removed *)
+let define evk body evd =
+  let evar_flags = remove_evar_flags evk evd.evar_flags in
+  define_gen evk body evd evar_flags
+
+(** In case of an evar-evar solution, the flags are inherited *)
+let define_with_evar evk body evd =
+  let evk' = fst (destEvar body) in
+  let evar_flags = inherit_evar_flags evd.evar_flags evk evk' in
+  let evd = unshelve evd [evk] in
+  let future_goals = FutureGoals.remove evk evd.future_goals in
+  let evd = { evd with future_goals } in
+  define_gen evk body evd evar_flags
+
+(* In case of restriction, we declare the aliasing and inherit the obligation
+   and typeclass flags. *)
+
+let restrict evk filter ?candidates ?src evd =
+  let evk' = new_untyped_evar () in
+  let evar_info = EvMap.find evk evd.undf_evars in
+  let id_inst = Filter.filter_list filter evar_info.evar_hyps.env_named_var in
+  let evar_info' =
+    { evar_info with evar_filter = filter;
+      evar_candidates = candidates;
+      evar_source = (match src with None -> evar_info.evar_source | Some src -> src);
+      evar_identity = Identity.make id_inst;
+    } in
+  let last_mods = match evd.conv_pbs with
+  | [] ->  evd.last_mods
+  | _ -> Evar.Set.add evk evd.last_mods in
+  let evar_names = EvNames.reassign_name_defined evk evk' evd.evar_names in
+  let body = mkEvar(evk',id_inst) in
+  let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
+  let evar_flags = inherit_evar_flags evd.evar_flags evk evk' in
+  let evd = { evd with undf_evars = EvMap.add evk' evar_info' undf_evars;
+    defn_evars; last_mods; evar_names; evar_flags }
+  in
+  (* Mark new evar as future goal, removing previous one,
+    circumventing Proofview.advance but making Proof.run_tactic catch these. *)
+  let evd = unshelve evd [evk] in
+  let evd = remove_future_goal evd evk in
+  let evd = declare_future_goal evk' evd in
+  (evd, evk')
 
 (**********************************************************)
 (* Accessing metas *)
@@ -1114,8 +1247,8 @@ let set_metas evd metas = {
   effects = evd.effects;
   evar_names = evd.evar_names;
   future_goals = evd.future_goals;
-  future_goals_status = evd.future_goals_status;
-  principal_future_goal = evd.principal_future_goal;
+  given_up = evd.given_up;
+  shelf = evd.shelf;
   extras = evd.extras;
 }