Imported Upstream version 8.5~beta1+dfsg

1 files changed, 206 insertions, 301 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index bd185b99..828f9fa7 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -1,16 +1,15 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
 (* Module defining the last essential tiles of interactive proofs.
-   The features of the Proof module are undoing and focusing.
-   A proof is a mutable object, it contains a proofview, and some information
-   to be able to undo actions, and to unfocus the current view. All three
-   of these being meant to evolve.
+   A proof deals with the focusing commands (including the braces and bullets),
+   the shelf (see the [shelve] tactic) and given up goal (see the [give_up]
+   tactic). A proof is made of the following:
    - Proofview: a proof is primarily the data of the current view.
      That which is shown to the user (as a remainder, a proofview
      is mainly the logical state of the proof, together with the
@@ -23,24 +22,27 @@
      the focus kind is actually stored inside the condition). To unfocus, one
      needs to know the focus kind, and the condition (for instance "no condition" or
      the proof under focused must be complete) must be met.
-   - Undo: since proofviews and focus stacks are immutable objects, 
-     it could suffice to hold the previous states, to allow to return to the past.
-     However, we also allow other modules to do actions that can be undone.
-     Therefore the undo stack stores action to be ran to undo.
+   - Shelf: A list of goals which have been put aside during the proof. They can be
+     retrieved with the [Unshelve] command, or solved by side effects
+   - Given up goals: as long as there is a given up goal, the proof is not completed.
+     Given up goals cannot be retrieved, the user must go back where the tactic
+     [give_up] was run and solve the goal there.
 *)
 
-open Term
+open Util
 
 type _focus_kind = int
 type 'a focus_kind = _focus_kind
 type focus_info = Obj.t
+type reason = NotThisWay | AlreadyNoFocus
 type unfocusable =
-  | Cannot of exn
+  | Cannot of reason
   | Loose
   | Strict
-type _focus_condition = 
-    (_focus_kind -> Proofview.proofview -> unfocusable) *
-    (_focus_kind -> bool)
+type _focus_condition =
+  | CondNo       of bool * _focus_kind
+  | CondDone     of bool * _focus_kind
+  | CondEndStack of        _focus_kind (* loose_end is false here *)
 type 'a focus_condition = _focus_condition
 
 let next_kind = ref 0
@@ -49,107 +51,71 @@ let new_focus_kind () =
   incr next_kind;
   r
 
-(* Auxiliary function to define conditions. *)
-let check kind1 kind2 = kind1=kind2
-
 (* To be authorized to unfocus one must meet the condition prescribed by
     the action which focused.*)
 (* spiwack: we could consider having a list of authorized focus_kind instead
     of just one, if anyone needs it *)
-(* [no_cond] only checks that the unfocusing command uses the right
-    [focus_kind]. *)
-
-module Cond = struct
-  (* first attempt at an algebra of condition *)
-  (* semantics:
-     - [Cannot] means that the condition is not met
-     - [Strict] that the condition is met
-     - [Loose] that the condition is not quite met
-       but authorises to unfocus provided a condition
-       of a previous focus on the stack is (strictly)
-       met. [Loose] focuses are those, like bullets,
-       which do not have a closing command and
-       are hence closed by unfocusing actions unrelated
-       to their focus_kind.
-  *)
-  let bool e b =
-    if b then fun _ _ -> Strict
-    else fun _ _ -> Cannot e
-  let loose c k p = match c k p with
-    | Cannot _ -> Loose
-    | c -> c
-  let cloose l c =
-    if l then loose c
-    else c
-  let (&&&) c1 c2 k p=
-    match c1 k p , c2 k p with
-    | Cannot e , _ 
-    | _ , Cannot e -> Cannot e
-    | Strict, Strict -> Strict
-    | _ , _ -> Loose
-  let kind e k0 k p = bool e (k0=k) k p 
-  let pdone e k p = bool e (Proofview.finished p) k p
-end
-
 
-(* Unfocus command.
-   Fails if the proof is not focused. *)
 exception CannotUnfocusThisWay
+
+(* Cannot focus on non-existing subgoals *)
+exception NoSuchGoals of int * int
+
+
+exception FullyUnfocused
+
 let _ = Errors.register_handler begin function
   | CannotUnfocusThisWay ->
-    Util.error "This proof is focused, but cannot be unfocused this way"
+    Errors.error "This proof is focused, but cannot be unfocused this way"
+  | NoSuchGoals (i,j) when Int.equal i j ->
+      Errors.errorlabstrm "Focus" Pp.(str"No such goal (" ++ int i ++ str").")
+  | NoSuchGoals (i,j) ->
+      Errors.errorlabstrm "Focus" Pp.(
+        str"Not every goal in range ["++ int i ++ str","++int j++str"] exist."
+      )
+  | FullyUnfocused -> Errors.error "The proof is not focused"
   | _ -> raise Errors.Unhandled
 end
 
-open Cond
-let no_cond_gen e ~loose_end k0 =
-  cloose loose_end (kind e k0)
-let no_cond_gen e ?(loose_end=false) k = no_cond_gen e ~loose_end k , check k
-let no_cond ?loose_end = no_cond_gen CannotUnfocusThisWay ?loose_end
-(* [done_cond] checks that the unfocusing command uses the right [focus_kind]
-    and that the focused proofview is complete. *)
-let done_cond_gen e ~loose_end k0 =
-  (cloose loose_end (kind e k0)) &&& pdone e
-let done_cond_gen e ?(loose_end=false) k = done_cond_gen e ~loose_end k , check k
-let done_cond ?loose_end = done_cond_gen CannotUnfocusThisWay ?loose_end
-
+let check_cond_kind c k =
+  let kind_of_cond = function
+    | CondNo (_,k) | CondDone(_,k) | CondEndStack k -> k in
+  Int.equal (kind_of_cond c) k
+
+let test_cond c k1 pw =
+  match c with
+  | CondNo(_,     k) when Int.equal k k1 -> Strict
+  | CondNo(true,  _)             -> Loose
+  | CondNo(false, _)             -> Cannot NotThisWay
+  | CondDone(_,     k) when Int.equal k k1 && Proofview.finished pw -> Strict
+  | CondDone(true,  _)                                      -> Loose
+  | CondDone(false, _)                                      -> Cannot NotThisWay
+  | CondEndStack k when Int.equal k k1 -> Strict
+  | CondEndStack _             -> Cannot AlreadyNoFocus
+
+let no_cond ?(loose_end=false) k = CondNo (loose_end, k)
+let done_cond ?(loose_end=false) k = CondDone (loose_end,k)
 
 (* Subpart of the type of proofs. It contains the parts of the proof which
    are under control of the undo mechanism *)
-type proof_state = {
+type proof = {
   (* Current focused proofview *)
   proofview: Proofview.proofview;
+  (* Entry for the proofview *)
+  entry : Proofview.entry;
   (* History of the focusings, provides information on how
      to unfocus the proof and the extra information stored while focusing.
      The list is empty when the proof is fully unfocused. *)
   focus_stack: (_focus_condition*focus_info*Proofview.focus_context) list;
-  (* Extra information which can be freely used to create new behaviours. *)
-  intel: Store.t
+  (* List of goals that have been shelved. *)
+  shelf : Goal.goal list;
+  (* List of goals that have been given up *)
+  given_up : Goal.goal list;
 }
 
-type proof_info = {
-  mutable endline_tactic : unit Proofview.tactic ;
-  mutable section_vars : Sign.section_context option;
-  initial_conclusions : Term.types list
-}
-
-type undo_action = 
-  | State of proof_state
-  | Effect of (unit -> unit)
-
-type proof = { (* current proof_state *)
-               mutable state : proof_state;
-               (* The undo stack *)
-               mutable undo_stack : undo_action list;
-	       (* secondary undo stacks used for transactions *)
-	       mutable transactions : undo_action list list;
-	       info : proof_info
-             }
-
-
 (*** General proof functions ***)
 
-let proof { state = p } =
+let proof p =
   let (goals,sigma) = Proofview.proofview p.proofview in
   (* spiwack: beware, the bottom of the stack is used by [Proof]
      internally, and should not be exposed. *)
@@ -161,322 +127,261 @@ let proof { state = p } =
   let stack =
     map_minus_one (fun (_,_,c) -> Proofview.focus_context c) p.focus_stack
   in
-  (goals,stack,sigma)
+  let shelf = p.shelf in
+  let given_up = p.given_up in
+  (goals,stack,shelf,given_up,sigma)
+
+type 'a pre_goals = {
+    fg_goals : 'a list;
+  (** List of the focussed goals *)
+  bg_goals : ('a list * 'a list) list;
+  (** Zipper representing the unfocussed background goals *)
+  shelved_goals : 'a list;
+  (** List of the goals on the shelf. *)
+  given_up_goals : 'a list;
+  (** List of the goals that have been given up *)
+}
+
+let map_structured_proof pfts process_goal: 'a pre_goals =
+  let (goals, zipper, shelf, given_up, sigma) = proof pfts in
+  let fg = List.map (process_goal sigma) goals in
+  let map_zip (lg, rg) =
+    let lg = List.map (process_goal sigma) lg in
+    let rg = List.map (process_goal sigma) rg in
+    (lg, rg)
+  in
+  let bg = List.map map_zip zipper in
+  let shelf = List.map (process_goal sigma) shelf in
+  let given_up = List.map (process_goal sigma) given_up in
+    { fg_goals = fg;
+      bg_goals = bg;
+      shelved_goals = shelf;
+      given_up_goals = given_up; }
 
 let rec unroll_focus pv = function
   | (_,_,ctx)::stk -> unroll_focus (Proofview.unfocus ctx pv) stk
   | [] -> pv
-
 (* spiwack: a proof is considered completed even if its still focused, if the focus
    doesn't hide any goal.
    Unfocusing is handled in {!return}. *)
 let is_done p =
-  Proofview.finished p.state.proofview && 
-  Proofview.finished (unroll_focus p.state.proofview p.state.focus_stack)
+  Proofview.finished p.proofview &&
+  Proofview.finished (unroll_focus p.proofview p.focus_stack)
 
 (* spiwack: for compatibility with <= 8.2 proof engine *)
 let has_unresolved_evar p =
-  Proofview.V82.has_unresolved_evar p.state.proofview
+  Proofview.V82.has_unresolved_evar p.proofview
 
 (* Returns the list of partial proofs to initial goals *)
-let partial_proof p =
-  List.map fst (Proofview.return p.state.proofview)
-
-
+let partial_proof p = Proofview.partial_proof p.entry p.proofview
 
 (*** The following functions implement the basic internal mechanisms
      of proofs, they are not meant to be exported in the .mli ***)
 
 (* An auxiliary function to push a {!focus_context} on the focus stack. *)
 let push_focus cond inf context pr =
-  pr.state <- { pr.state with focus_stack = (cond,inf,context)::pr.state.focus_stack }
+  { pr with focus_stack = (cond,inf,context)::pr.focus_stack }
 
-exception FullyUnfocused
-let _ = Errors.register_handler begin function
-  | FullyUnfocused -> Util.error "The proof is not focused"
-  | _ -> raise Errors.Unhandled
-end
 (* An auxiliary function to read the kind of the next focusing step *)
 let cond_of_focus pr =
-  match pr.state.focus_stack with
+  match pr.focus_stack with
   | (cond,_,_)::_ -> cond
   | _ -> raise FullyUnfocused
 
 (* An auxiliary function to pop and read the last {!Proofview.focus_context} 
    on the focus stack. *)
 let pop_focus pr =
-  match pr.state.focus_stack with
-  | focus::other_focuses -> 
-      pr.state <- { pr.state with focus_stack = other_focuses }; focus
-  | _ -> 
+  match pr.focus_stack with
+  | focus::other_focuses ->
+      { pr with focus_stack = other_focuses }, focus
+  | _ ->
       raise FullyUnfocused
 
-(* Auxiliary function to push a [proof_state] onto the undo stack. *)
-let push_undo save pr =
-  match pr.transactions with
-  | [] -> pr.undo_stack <- save::pr.undo_stack
-  | stack::trans' -> pr.transactions <- (save::stack)::trans'
-
-(* Auxiliary function to pop and read a [save_state] from the undo stack. *)
-exception EmptyUndoStack
-let _ = Errors.register_handler begin function
-  | EmptyUndoStack -> Util.error "Cannot undo: no more undo information"
-  | _ -> raise Errors.Unhandled
-end
-let pop_undo pr =
-  match pr.transactions , pr.undo_stack with
-  | [] , state::stack -> pr.undo_stack <- stack; state
-  | (state::stack)::trans', _ -> pr.transactions <- stack::trans'; state
-  | _ -> raise EmptyUndoStack
-
-
 (* This function focuses the proof [pr] between indices [i] and [j] *)
 let _focus cond inf i j pr =
-  let (focused,context) = Proofview.focus i j pr.state.proofview in
-  push_focus cond inf context pr;
-  pr.state <- { pr.state with proofview = focused }
+  let focused, context = Proofview.focus i j pr.proofview in
+  let pr = push_focus cond inf context pr in
+  { pr with proofview = focused }
 
 (* This function unfocuses the proof [pr], it raises [FullyUnfocused],
    if the proof is already fully unfocused.
    This function does not care about the condition of the current focus. *)
 let _unfocus pr =
-  let (_,_,fc) = pop_focus pr in
-  pr.state <- { pr.state with proofview = Proofview.unfocus fc pr.state.proofview }
-
-
-let set_used_variables l p =
-  p.info.section_vars <- Some l
-
-let get_used_variables p = p.info.section_vars
-
-(*** Endline tactic ***)
-
-(* spiwack this is an information about the UI, it might be a good idea to move
-   it to the Proof_global module *)
-
-(* Sets the tactic to be used when a tactic line is closed with [...] *)
-let set_endline_tactic tac p =
- p.info.endline_tactic <- tac
-
-let with_end_tac pr tac =
-  Proofview.tclTHEN tac pr.info.endline_tactic
-
-(*** The following functions define the safety mechanism of the
-     proof system, they may be unsafe if not used carefully. There is
-     currently no reason to export them in the .mli ***)
-
-(* This functions saves the current state into a [proof_state]. *)
-let save_state { state = ps } = State ps
-
-(* This function stores the current proof state in the undo stack. *)
-let save pr =
-  push_undo (save_state pr) pr
-
-(* This function restores a state, presumably from the top of the undo stack. *)
-let restore_state save pr =
-  match save with
-  | State save -> pr.state <- save
-  | Effect undo -> undo ()
-
-(* Interpretes the Undo command. *)
-let undo pr =
-  (* On a single line, since the effects commute *)
-  restore_state (pop_undo pr) pr
-
-(* Adds an undo effect to the undo stack. Use it with care, errors here might result
-    in inconsistent states. *)
-let add_undo effect pr =
-  push_undo (Effect effect) pr
-
-
-
-(*** Transactions ***)
-
-let init_transaction pr =
-  pr.transactions <- []::pr.transactions
-
-let commit_stack pr stack =
-  let push s = push_undo s pr in
-  List.iter push (List.rev stack)
-
-(* Invariant: [commit] should be called only when a transaction
-   is open. It closes the current transaction. *)
-let commit pr =
-  match pr.transactions with
-  | stack::trans' ->
-    pr.transactions <- trans';
-    commit_stack pr stack
-  | [] -> assert false
-
-(* Invariant: [rollback] should be called only when a transaction
-   is open. It closes the current transaction. *)
-let rec rollback pr =
-  try
-    undo pr;
-    rollback pr
-  with EmptyUndoStack ->
-    match pr.transactions with
-    | []::trans' -> pr.transactions <- trans'
-    | _ -> assert false
-
-
-let transaction pr t =
-  init_transaction pr;
-  try t (); commit pr
-  with reraise -> rollback pr; raise reraise
-
+  let pr, (_,_,fc) = pop_focus pr in
+   { pr with proofview = Proofview.unfocus fc pr.proofview }
 
 (* Focus command (focuses on the [i]th subgoal) *)
 (* spiwack: there could also, easily be a focus-on-a-range tactic, is there 
    a need for it? *)
 let focus cond inf i pr =
-  save pr;
-  _focus cond (Obj.repr inf) i i pr
+  try _focus cond (Obj.repr inf) i i pr
+  with CList.IndexOutOfRange -> raise (NoSuchGoals (i,i))
 
 let rec unfocus kind pr () =
-  let starting_point = save_state pr in
   let cond = cond_of_focus pr in
-  match fst cond kind pr.state.proofview with
-  | Cannot e -> raise e
-  | Strict -> 
-    (_unfocus pr;
-     push_undo starting_point pr)
+  match test_cond cond kind pr.proofview with
+  | Cannot NotThisWay -> raise CannotUnfocusThisWay
+  | Cannot AlreadyNoFocus -> raise FullyUnfocused
+  | Strict ->
+     let pr = _unfocus pr in
+     pr
   | Loose ->
     begin try
-	    _unfocus pr;
-	    push_undo starting_point pr;
+            let pr = _unfocus pr in
 	    unfocus kind pr ()
       with FullyUnfocused -> raise CannotUnfocusThisWay
     end
 
-let unfocus kind pr =
-  transaction pr (unfocus kind pr)
-
 exception NoSuchFocus
 (* no handler: should not be allowed to reach toplevel. *)
 let rec get_in_focus_stack kind stack =
   match stack with
-  | ((_,check),inf,_)::stack ->
-      if check kind then inf
+  | (cond,inf,_)::stack ->
+      if check_cond_kind cond kind then inf
       else get_in_focus_stack kind stack
   | [] -> raise NoSuchFocus
 let get_at_focus kind pr =
-  Obj.magic (get_in_focus_stack kind pr.state.focus_stack)
+  Obj.magic (get_in_focus_stack kind pr.focus_stack)
 
 let is_last_focus kind pr =
-  let ((_,check),_,_) = List.hd pr.state.focus_stack in
-  check kind
+  let (cond,_,_) = List.hd pr.focus_stack in
+  check_cond_kind cond kind
 
 let no_focused_goal p =
-  Proofview.finished p.state.proofview
+  Proofview.finished p.proofview
+
+let rec maximal_unfocus k p =
+  if no_focused_goal p then
+    try maximal_unfocus k (unfocus k p ())
+    with FullyUnfocused | CannotUnfocusThisWay -> p
+  else p
 
 (*** Proof Creation/Termination ***)
 
 (* [end_of_stack] is unfocused by return to close every loose focus. *)
 let end_of_stack_kind = new_focus_kind ()
-let end_of_stack = done_cond_gen FullyUnfocused end_of_stack_kind
+let end_of_stack = CondEndStack end_of_stack_kind
 
 let unfocused = is_last_focus end_of_stack_kind
 
-let start goals =
-  let pr =
-    { state = { proofview = Proofview.init goals ;
-	        focus_stack = [] ;
-	        intel = Store.empty} ;
-      undo_stack = [] ;
-      transactions = [] ;
-      info = { endline_tactic = Proofview.tclUNIT ();
-               initial_conclusions = List.map snd goals;
-               section_vars = None }
-    }
-  in
-  _focus end_of_stack (Obj.repr ()) 1 (List.length goals) pr;
-  pr
+let start sigma goals =
+  let entry, proofview = Proofview.init sigma goals in
+  let pr = {
+    proofview;
+    entry;
+    focus_stack = [] ;
+    shelf = [] ;
+    given_up = [] } in
+  _focus end_of_stack (Obj.repr ()) 1 (List.length goals) pr
+let dependent_start goals =
+  let entry, proofview = Proofview.dependent_init goals in
+  let pr = {
+    proofview;
+    entry;
+    focus_stack = [] ;
+    shelf = [] ;
+    given_up = [] } in
+  let number_of_goals = List.length (Proofview.initial_goals pr.entry) in
+  _focus end_of_stack (Obj.repr ()) 1 number_of_goals pr
 
 exception UnfinishedProof
+exception HasShelvedGoals
+exception HasGivenUpGoals
 exception HasUnresolvedEvar
 let _ = Errors.register_handler begin function
-  | UnfinishedProof -> Util.error "Some goals have not been solved."
-  | HasUnresolvedEvar -> Util.error "Some existential variables are uninstantiated."
+  | UnfinishedProof -> Errors.error "Some goals have not been solved."
+  | HasShelvedGoals -> Errors.error "Some goals have been left on the shelf."
+  | HasGivenUpGoals -> Errors.error "Some goals have been given up."
+  | HasUnresolvedEvar -> Errors.error "Some existential variables are uninstantiated."
   | _ -> raise Errors.Unhandled
 end
+
 let return p =
   if not (is_done p) then
     raise UnfinishedProof
-  else if has_unresolved_evar p then 
+  else if not (CList.is_empty (p.shelf)) then
+    raise HasShelvedGoals
+  else if not (CList.is_empty (p.given_up)) then
+    raise HasGivenUpGoals
+  else if has_unresolved_evar p then
     (* spiwack: for compatibility with <= 8.3 proof engine *)
     raise HasUnresolvedEvar
   else
-    unfocus end_of_stack_kind p;
-    Proofview.return p.state.proofview
-
-(*** Function manipulation proof extra informations ***)
+    let p = unfocus end_of_stack_kind p () in
+    Proofview.return p.proofview
 
-let get_proof_info pr =
-  pr.state.intel
+let initial_goals p = Proofview.initial_goals p.entry
 
-let set_proof_info info pr =
-  save pr;
-  pr.state <- { pr.state with intel=info }
+let compact p =
+  let entry, proofview = Proofview.compact p.entry p.proofview in
+  { p with proofview; entry }
 
+(*** Function manipulation proof extra informations ***)
 
 (*** Tactics ***)
 
 let run_tactic env tac pr =
-  let starting_point = save_state pr in
-  let sp = pr.state.proofview in
-  try
-    let tacticced_proofview = Proofview.apply env tac sp in
-    pr.state <- { pr.state with proofview = tacticced_proofview };
-    push_undo starting_point pr
-  with reraise ->
-    restore_state starting_point pr;
-    raise reraise
+  let sp = pr.proofview in
+  let (_,tacticced_proofview,(status,to_shelve,give_up),info_trace) =
+    Proofview.apply env tac sp
+  in
+  let sigma = Proofview.return tacticced_proofview in
+  (* Already solved goals are not to be counted as shelved. Nor are
+     they to be marked as unresolvable. *)
+  let undef l = List.filter (fun g -> Evd.is_undefined sigma g) l in
+  let retrieved = undef (List.rev (Evd.future_goals sigma)) in
+  let shelf = (undef pr.shelf)@retrieved@(undef to_shelve) in
+  let proofview =
+    List.fold_left
+      Proofview.Unsafe.mark_as_goal
+      tacticced_proofview
+      retrieved
+  in
+  let given_up = pr.given_up@give_up in
+  let proofview = Proofview.Unsafe.reset_future_goals proofview in
+  { pr with proofview ; shelf ; given_up },(status,info_trace)
 
 (*** Commands ***)
 
-let in_proof p k =
-  Proofview.in_proofview p.state.proofview k
+let in_proof p k = k (Proofview.return p.proofview)
 
+(* Remove all the goals from the shelf and adds them at the end of the
+   focused goals. *)
+let unshelve p =
+  { p with proofview = Proofview.unshelve (p.shelf) (p.proofview) ; shelf = [] }
 
 (*** Compatibility layer with <=v8.2 ***)
 module V82 = struct
   let subgoals p =
-    Proofview.V82.goals p.state.proofview
+    Proofview.V82.goals p.proofview
 
   let background_subgoals p =
-    Proofview.V82.goals (unroll_focus p.state.proofview p.state.focus_stack)
-
-  let get_initial_conclusions p = 
-    p.info.initial_conclusions
-
-  let depth p = List.length p.undo_stack
+    Proofview.V82.goals (unroll_focus p.proofview p.focus_stack)
 
-  let top_goal p = 
-    let { Evd.it=gls ; sigma=sigma } = 
-	Proofview.V82.top_goals p.state.proofview
+  let top_goal p =
+    let { Evd.it=gls ; sigma=sigma; } =
+	Proofview.V82.top_goals p.entry p.proofview
     in
-    { Evd.it=List.hd gls ; sigma=sigma }
+    { Evd.it=List.hd gls ; sigma=sigma; }
 
   let top_evars p =
-    Proofview.V82.top_evars p.state.proofview
+    Proofview.V82.top_evars p.entry
 
   let grab_evars p =
     if not (is_done p) then
       raise UnfinishedProof
     else
-      save p;
-      p.state <- { p.state with proofview = Proofview.V82.grab p.state.proofview }
-    
-
-    let instantiate_evar n com pr =
-      let starting_point = save_state pr in
-      let sp = pr.state.proofview in
-      try
-	let new_proofview = Proofview.V82.instantiate_evar n com sp in
-	pr.state <- { pr.state with proofview = new_proofview };
-	push_undo starting_point pr
-      with reraise ->
-	restore_state starting_point pr;
-	raise reraise
+      { p with proofview = Proofview.V82.grab p.proofview }
+
+
+  let instantiate_evar n com pr =
+    let sp = pr.proofview in
+    let proofview = Proofview.V82.instantiate_evar n com sp in
+    let shelf =
+      List.filter begin fun g ->
+        Evd.is_undefined (Proofview.return proofview) g
+      end pr.shelf
+    in
+    { pr with proofview ; shelf }
+
 end