Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2

20 files changed, 229 insertions, 210 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index d06c6f2e..b98101e0 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -500,8 +500,8 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function
       let clause = mk_clenv_from_env env sigma n (c,t) in
       clenv_constrain_dep_args hyps_only largs clause
   | ExplicitBindings lbind ->
-      let clause = mk_clenv_from_env env sigma n 
-	(c,rename_bound_vars_as_displayed [] t) 
+      let clause = mk_clenv_from_env env sigma n
+	(c,rename_bound_vars_as_displayed [] [] t)
       in clenv_match_args lbind clause
   | NoBindings ->
       mk_clenv_from_env env sigma n (c,t)
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 36268de1..6fa95dc8 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -40,7 +40,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
     error "Instantiate called on already-defined evar";
   let env = Evd.evar_env evi in
   let sigma',typed_c =
-    try Pretyping.Default.understand_ltac true sigma env ltac_var
+    try Pretyping.Default.understand_ltac ~resolve_classes:true true sigma env ltac_var
 	  (Pretyping.OfType (Some evi.evar_concl)) rawc
     with _ ->
       let loc = Glob_term.loc_of_glob_constr rawc in
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 1542267e..eeaba76e 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -163,8 +163,8 @@ module Refinable = struct
   (* spiwack: it is not very fine grain since it solves all typeclasses holes, 
       not only those containing the current goal, or a given term. But it
       seems to fit our needs so far. *)
-  let resolve_typeclasses ?onlyargs ?split ?(fail=false) () env rdefs _ _ =
-    rdefs:=Typeclasses.resolve_typeclasses ?onlyargs ?split ~fail env !rdefs;
+  let resolve_typeclasses ?filter ?split ?(fail=false) () env rdefs _ _ =
+    rdefs:=Typeclasses.resolve_typeclasses ?filter ?split ~fail env !rdefs;
     ()
 
 
@@ -563,7 +563,7 @@ module V82 = struct
     let new_sigma = Evd.add Evd.empty evk new_evi in
     { Evd.it = build evk ; sigma = new_sigma }
 
-  (* Used by the typeclasses *)
+  (* Used by the compatibility layer and typeclasses *)
   let nf_evar sigma gl =
     let evi = content sigma gl in
     let evi = Evarutil.nf_evar_info sigma evi in
diff --git a/proofs/goal.mli b/proofs/goal.mli
index e9d23065..50709555 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -72,7 +72,7 @@ module Refinable : sig
   (* [with_type c typ] constrains term [c] to have type [typ].  *)
   val with_type : Term.constr -> Term.types -> Term.constr sensitive
 
-  val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool -> unit -> unit sensitive
+  val resolve_typeclasses : ?filter:(Evd.hole_kind -> bool) -> ?split:bool -> ?fail:bool -> unit -> unit sensitive
 
 
   (* [constr_of_raw h check_type resolve_classes] is a pretyping function.
@@ -234,7 +234,7 @@ module V82 : sig
  (* Used for congruence closure *)
   val new_goal_with : Evd.evar_map -> goal ->  Environ.named_context_val -> goal Evd.sigma 
 
-  (* Used by the typeclasses *)
+  (* Used by the compatibility layer and typeclasses *)
   val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map
 
   (* Goal represented as a type, doesn't take into account section variables *)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index a363c6bb..5babd03a 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -685,12 +685,8 @@ let prim_refiner r sigma goal =
           ([gl], sigma)
 
     | Change_evars ->
-	(* spiwack: a priori [Change_evars] is now devoid of operational content.
-	    The new proof engine keeping the evar_map up to date at all time.
-	    As a compatibility mesure I leave the rule. 
-	    It is possible that my assumption is wrong and some uses of 
-	    [Change_evars] are not subsumed by the new engine. In which
-	    case something has to be done here. (Feb. 2010) *)
+	(* Normalises evars in goals. Used by instantiate. *)
+        let (goal,sigma) = Goal.V82.nf_evar sigma goal in
 	([goal],sigma)
 
 (************************************************************************)
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 3d507f35..6ac0b553 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -35,8 +35,10 @@ let delete_proof = Proof_global.discard
 let delete_current_proof = Proof_global.discard_current
 let delete_all_proofs = Proof_global.discard_all
 
-let undo n = 
+let undo n =
   let p = Proof_global.give_me_the_proof () in
+  let d = Proof.V82.depth p in
+  if n >= d then raise Proof.EmptyUndoStack;
   for i = 1 to n do
     Proof.undo p
   done
@@ -64,15 +66,7 @@ let start_proof id str hyps c ?init_tac ?compute_guard hook =
   Proof_global.start_proof id str goals ?compute_guard hook;
   Option.iter Proof_global.run_tactic init_tac
 
-let restart_proof () =
-  let p = Proof_global.give_me_the_proof () in
-  try while true do
-    Proof.undo p
-  done with Proof.EmptyUndoStack -> ()
-
-let resume_last_proof () = Proof_global.resume_last ()
-let resume_proof (_,id) = Proof_global.resume id
-let suspend_proof ()  =  Proof_global.suspend ()
+let restart_proof () = undo_todepth 1
 
 let cook_proof hook =
   let prf = Proof_global.give_me_the_proof () in
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 7297b975..5d45ea7c 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -85,24 +85,6 @@ val start_proof :
 val restart_proof : unit -> unit
 
 (** {6 ... } *)
-(** [resume_last_proof ()] focus on the last unfocused proof or fails
-   if there is no suspended proofs *)
-
-val resume_last_proof : unit -> unit
-
-(** [resume_proof name] focuses on the proof of name [name] or
-   raises [NoSuchProof] if no proof has name [name]. 
-
-    It doesn't [suspend_proof ()] before. *)
-
-val resume_proof : identifier located -> unit
-
-(** [suspend_proof ()] unfocuses the current focused proof or
-   failed with [UserError] if no proof is currently focused *)
-
-val suspend_proof : unit -> unit
-
-(** {6 ... } *)
 (** [cook_proof opacity] turns the current proof (assumed completed) into
     a constant with its name, kind and possible hook (see [start_proof]);
     it fails if there is no current proof of if it is not completed;
@@ -143,7 +125,9 @@ val current_proof_statement :
 
 val get_current_proof_name : unit -> identifier
 
-(** [get_all_proof_names ()] returns the list of all pending proof names *)
+(** [get_all_proof_names ()] returns the list of all pending proof names.
+    The first name is the current proof, the other names may come in
+    any order. *)
 
 val get_all_proof_names : unit -> identifier list
 
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 72730495..996a895f 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -35,12 +35,12 @@ type _focus_kind = int
 type 'a focus_kind = _focus_kind
 type focus_info = Obj.t
 type unfocusable =
-  | Cannot
+  | Cannot of exn
   | Loose
   | Strict
 type _focus_condition = 
     (_focus_kind -> Proofview.proofview -> unfocusable) *
-    (_focus_kind -> focus_info -> focus_info)
+    (_focus_kind -> bool)
 type 'a focus_condition = _focus_condition
 
 let next_kind = ref 0
@@ -49,13 +49,8 @@ let new_focus_kind () =
   incr next_kind;
   r
 
-(* Auxiliary function to define conditions:
-   [check kind1 kind2 inf] returns [inf] if [kind1] and [kind2] match.
-   Otherwise it raises [CheckNext] *)
-exception CheckNext
-(* no handler: confined to this module. *)
-let check kind1 kind2 inf =
-  if kind1=kind2 then inf else raise CheckNext
+(* 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.*)
@@ -68,40 +63,55 @@ module Cond = struct
   (* first attempt at an algebra of condition *)
   (* semantics:
      - [Cannot] means that the condition is not met
-     - [Strict] that the condition is meant
-     - [Loose] that the condition is not quite meant
+     - [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.
+       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 b =
+  let bool e b =
     if b then fun _ _ -> Strict
-    else fun _ _ -> Cannot
+    else fun _ _ -> Cannot e
   let loose c k p = match c k p with
-    | Cannot -> Loose
+    | 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 , _ 
-    | _ , Cannot -> Cannot
+    | Cannot e , _ 
+    | _ , Cannot e -> Cannot e
     | Strict, Strict -> Strict
     | _ , _ -> Loose
-  let kind k0 k p = bool (k0=k) k p 
-  let pdone k p = bool (Proofview.finished p) k p
+  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
+let _ = Errors.register_handler begin function
+  | CannotUnfocusThisWay ->
+    Util.error "This proof is focused, but cannot be unfocused this way"
+  | _ -> raise Errors.Unhandled
 end
 
 open Cond
-let no_cond ~loose_end k0 =
-  cloose loose_end (kind k0)
-let no_cond ?(loose_end=false) k = no_cond ~loose_end k , check k
+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 ~loose_end k0 =
-  (cloose loose_end (kind k0)) &&& pdone
-let done_cond ?(loose_end=false) k = done_cond ~loose_end k , check k
+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
 
 
 (* Subpart of the type of proofs. It contains the parts of the proof which
@@ -249,13 +259,13 @@ 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 = 
+let restore_state save pr =
   match save with
   | State save -> pr.state <- save
   | Effect undo -> undo ()
 
 (* Interpretes the Undo command. *)
-let undo pr = 
+let undo pr =
   (* On a single line, since the effects commute *)
   restore_state (pop_undo pr) pr
 
@@ -309,20 +319,11 @@ let focus cond inf i pr =
   save pr;
   _focus cond (Obj.repr inf) i i pr
 
-(* Unfocus command.
-   Fails if the proof is not focused. *)
-exception CannotUnfocusThisWay
-let _ = Errors.register_handler begin function
-  | CannotUnfocusThisWay ->
-    Util.error "This proof is focused, but cannot be unfocused this way"
-  | _ -> raise Errors.Unhandled
-end
-
 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 -> raise CannotUnfocusThisWay
+  | Cannot e -> raise e
   | Strict -> 
     (_unfocus pr;
      push_undo starting_point pr)
@@ -336,34 +337,35 @@ let rec unfocus kind pr () =
 
 let unfocus kind pr =
   transaction pr (unfocus kind pr)
-      
-let get_at_point kind ((_,get),inf,_) = get kind inf
+
 exception NoSuchFocus
 (* no handler: should not be allowed to reach toplevel. *)
-exception GetDone of Obj.t
-(* no handler: confined to this module. *)
-let get_in_focus_stack kind stack =
-  try
-    List.iter begin fun pt ->
-      try 
-	raise (GetDone (get_at_point kind pt))
-      with CheckNext -> ()
-    end stack;
-    raise NoSuchFocus
-  with GetDone x -> x
+let rec get_in_focus_stack kind stack =
+  match stack with
+  | ((_,check),inf,_)::stack ->
+      if check 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)
 
+let is_last_focus kind pr =
+  let ((_,check),_,_) = List.hd pr.state.focus_stack in
+  check kind
+
 let no_focused_goal p =
   Proofview.finished p.state.proofview
 
 (*** 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 end_of_stack_kind
+let end_of_stack = done_cond_gen FullyUnfocused end_of_stack_kind
+
+let unfocused = is_last_focus end_of_stack_kind
 
 let start goals =
-  let pr = 
+  let pr =
     { state = { proofview = Proofview.init goals ;
 	        focus_stack = [] ;
 	        intel = Store.empty} ;
@@ -445,14 +447,22 @@ module V82 = struct
   let top_evars p =
     Proofview.V82.top_evars 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 e -> 
-      restore_state starting_point pr;
-      raise e
+  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 e -> 
+	restore_state starting_point pr;
+	raise e
 end
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 12af18f4..715b3341 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -114,12 +114,18 @@ exception CannotUnfocusThisWay
      is not met. *)
 val unfocus : 'a focus_kind -> proof -> unit
 
+(* [unfocused p] returns [true] when [p] is fully unfocused. *)
+val unfocused : proof -> bool
+
 (* [get_at_focus k] gets the information stored at the closest focus point
     of kind [k].
     Raises [NoSuchFocus] if there is no focus point of kind [k]. *)
 exception NoSuchFocus
 val get_at_focus : 'a focus_kind -> proof -> 'a
 
+(* [is_last_focus k] check if the most recent focus is of kind [k] *)
+val is_last_focus : 'a focus_kind -> proof -> bool
+
 (* returns [true] if there is no goal under focus. *)
 val no_focused_goal : proof -> bool
 
@@ -127,8 +133,6 @@ val no_focused_goal : proof -> bool
 
 val get_proof_info : proof -> Store.t
 
-val set_proof_info : Store.t -> proof -> unit
-
 (* Sets the section variables assumed by the proof *)
 val set_used_variables : Sign.section_context -> proof -> unit
 val get_used_variables : proof -> Sign.section_context option
@@ -151,7 +155,7 @@ val run_tactic : Environ.env -> unit Proofview.tactic -> proof -> unit
    a focusing command and a tactic. Transactions are such that if
    any of the atomic action fails, the whole transaction fails.
 
-   During a transaction, the undo visible undo stack is constituted only
+   During a transaction, the visible undo stack is constituted only
    of the actions performed done during the transaction.
 
    [transaction p f] can be called on an [f] using, itself, [transaction p].*)
@@ -178,6 +182,10 @@ module V82 : sig
   (* returns the existential variable used to start the proof *)
   val top_evars : proof -> Evd.evar list
 
+  (* Turns the unresolved evars into goals.
+     Raises [UnfinishedProof] if there are still unsolved goals. *)
+  val grab_evars : proof -> unit
+
   (* Implements the Existential command *)
   val instantiate_evar : int -> Topconstr.constr_expr -> proof -> unit
 end
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 2745270a..ae0f7d12 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -70,12 +70,10 @@ type proof_info = {
   mode : proof_mode
 }
 
-(* Invariant: a proof is at most in one of current_proof and suspended. And the 
-   domain of proof_info is the union of that of current_proof and suspended.*)
-(* The head of [!current_proof] is the actual current proof, the other ones are to
-    be resumed when the current proof is closed, aborted or suspended. *)
+(* Invariant: the domain of proof_info is current_proof.*)
+(* The head of [!current_proof] is the actual current proof, the other ones are
+   to be resumed when the current proof is closed or aborted. *)
 let current_proof = ref ([]:nproof list)
-let suspended = ref ([] : nproof list)
 let proof_info = ref (Idmap.empty : proof_info Idmap.t)
 
 (* Current proof_mode, for bookkeeping *)
@@ -93,7 +91,7 @@ let update_proof_mode () =
       !current_proof_mode.reset (); 
       current_proof_mode := standard
 
-(* combinators for the current_proof and suspended lists *)
+(* combinators for the current_proof lists *)
 let push a l = l := a::!l;
   update_proof_mode ()
 
@@ -145,8 +143,7 @@ let remove id m =
 (*** Proof Global manipulation ***)
 
 let get_all_proof_names () =
-    List.map fst !current_proof @
-    List.map fst !suspended
+    List.map fst !current_proof
 
 let give_me_the_proof () = 
   snd (find_top current_proof)
@@ -160,61 +157,40 @@ let get_current_proof_name () =
     accessed directly through vernacular commands. Error message should be 
    pushed to external layers, and so we should be able to have a finer
    control on error message on complex actions. *)
-let msg_proofs use_resume =
+let msg_proofs () =
   match get_all_proof_names () with
     | [] -> (spc () ++ str"(No proof-editing in progress).")
     | l ->  (str"." ++ fnl () ++ str"Proofs currently edited:" ++ spc () ++
-               (Util.prlist_with_sep Util.pr_spc Nameops.pr_id l) ++
-	       str"." ++
-               (if use_resume then (fnl () ++ str"Use \"Resume\" first.")
-              	else (mt ()))
-	    )
-
+               (Util.prlist_with_sep Util.pr_spc Nameops.pr_id l)++ str ".")
 
 let there_is_a_proof () = !current_proof <> []
-let there_are_suspended_proofs () = !suspended <> []
-let there_are_pending_proofs () = 
-  there_is_a_proof () || 
-  there_are_suspended_proofs ()
-let check_no_pending_proof () = 
+let there_are_pending_proofs () = there_is_a_proof ()
+let check_no_pending_proof () =
   if not (there_are_pending_proofs ()) then
     ()
   else begin
     Util.error (Pp.string_of_ppcmds
-      (str"Proof editing in progress" ++ (msg_proofs false) ++ fnl() ++
+      (str"Proof editing in progress" ++ msg_proofs () ++ fnl() ++
        str"Use \"Abort All\" first or complete proof(s)."))
   end
 
-
-let suspend () =
-  rotate_top current_proof suspended
-
-let resume_last () =
-  rotate_top suspended current_proof
-
-let resume id =
-  rotate_find id suspended current_proof
-
 let discard_gen id =
-  try 
-    ignore (extract id current_proof);
-    remove id proof_info
-  with NoSuchProof -> ignore (extract id suspended)
+  ignore (extract id current_proof);
+  remove id proof_info
 
 let discard (loc,id) = 
   try
     discard_gen id
   with NoSuchProof ->
     Util.user_err_loc
-      (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs false)
+      (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs ())
 
 let discard_current () =
   let (id,_) = extract_top current_proof in
   remove id proof_info
  
 let discard_all () =
-  current_proof := []; 
-  suspended := [];
+  current_proof := [];
   proof_info := Idmap.empty
 
 (* [set_proof_mode] sets the proof mode to be used after it's called. It is
@@ -239,6 +215,11 @@ let set_proof_mode mn =
   end pr ;
   set_proof_mode m id
 
+exception AlreadyExists
+let _ = Errors.register_handler begin function
+  | AlreadyExists -> Util.error "Already editing something of that name."
+  | _ -> raise Errors.Unhandled
+end
 (* [start_proof s str env t hook tac] starts a proof of name [s] and
     conclusion [t]; [hook] is optionally a function to be applied at
     proof end (e.g. to declare the built constructions as a coercion
@@ -248,7 +229,11 @@ let set_proof_mode mn =
     It raises exception [ProofInProgress] if there is a proof being
     currently edited. *)
 let start_proof  id str goals ?(compute_guard=[]) hook =
-  (* arnaud: ajouter une vérification pour la présence de id dans le proof_global *)
+  begin
+    List.iter begin fun (id_ex,_) ->
+      if Names.id_ord id id_ex = 0 then raise AlreadyExists
+    end !current_proof
+  end;
   let p = Proof.start goals in
   add id { strength=str ; 
 	        compute_guard=compute_guard ; 
@@ -354,9 +339,14 @@ module Bullet = struct
     let bullet_kind = (Proof.new_focus_kind () : t list Proof.focus_kind)
     let bullet_cond = Proof.done_cond ~loose_end:true bullet_kind
 
+    (* spiwack: as it is bullets are reset (locally) by *any* non-bullet focusing command
+       experience will tell if this is the right discipline of if we want to be finer and
+       reset them only for a choice of bullets. *)
     let get_bullets pr =
-      try Proof.get_at_focus bullet_kind pr
-      with Proof.NoSuchFocus -> []
+      if Proof.is_last_focus bullet_kind pr then
+	Proof.get_at_focus bullet_kind pr
+      else
+	[]
 
     let has_bullet bul pr =
       let rec has_bullet = function
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index ed6a60c7..e266d57c 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -69,12 +69,6 @@ val close_proof : unit ->
 
 exception NoSuchProof
 
-val suspend : unit -> unit
-val resume_last : unit -> unit
-
-val resume : Names.identifier -> unit
-(** @raise NoSuchProof if it doesn't find one. *)
-
 (** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is 
    no current proof. *)
 val run_tactic : unit Proofview.tactic -> unit
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 0d50d521..4246cc9c 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -475,6 +475,17 @@ module V82 = struct
   let has_unresolved_evar pv =
     Evd.has_undefined pv.solution
 
+  (* Main function in the implementation of Grab Existential Variables.*)
+  let grab pv =
+    let goals =
+      List.map begin fun (e,_) ->
+	Goal.build e
+      end (Evd.undefined_list pv.solution)
+    in
+    { pv with comb = goals }
+      
+    
+
   (* Returns the open goals of the proofview together with the evar_map to 
      interprete them. *)
   let goals { comb = comb ; solution = solution } = 
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 24da9d77..fe24b54b 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -195,6 +195,11 @@ module V82 : sig
 
   val has_unresolved_evar : proofview -> bool
 
+  (* Main function in the implementation of Grab Existential Variables.
+     Resets the proofview's goals so that it contains all unresolved evars
+     (in chronological order of insertion). *)
+  val grab : proofview -> proofview
+
   (* Returns the open goals of the proofview together with the evar_map to 
      interprete them. *)
   val goals : proofview -> Goal.goal list Evd.sigma
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 5cd85547..8901a5a2 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -415,10 +415,6 @@ let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma}
 let pp_info = ref (fun _ _ _ -> assert false)
 let set_info_printer f = pp_info := f
 
-let tclINFO (tac : tactic) gls =
-  msgnl (hov 0 (str "Warning: info is currently not working"));
-  tac gls
-
 (* Check that holes in arguments have been resolved *)
 
 let check_evars env sigma extsigma gl =
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 75fd6d3d..9d3d37c2 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -137,7 +137,6 @@ val tclTIMEOUT       : int -> tactic -> tactic
 val tclWEAK_PROGRESS : tactic -> tactic
 val tclPROGRESS      : tactic -> tactic
 val tclNOTSAMEGOAL   : tactic -> tactic
-val tclINFO          : tactic -> tactic
 
 (** [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then,
    if it succeeds, applies [tac2] to the resulting subgoals,
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index b8279b8f..de2e662f 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -27,6 +27,8 @@ type split_flag = bool     (* true = exists           false = split *)
 type hidden_flag = bool    (* true = internal use     false = user-level *)
 type letin_flag = bool     (* true = use local def    false = use Leibniz *)
 
+type debug = Debug | Info | Off (* for trivial / auto / eauto ... *)
+
 type glob_red_flag =
   | FBeta
   | FIota
@@ -171,13 +173,8 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_atomic_tactic_expr =
   | TacLApply of 'constr
 
   (* Automation tactics *)
-  | TacTrivial of 'constr list * string list option
-  | TacAuto of int or_var option * 'constr list * string list option
-  | TacAutoTDB of int option
-  | TacDestructHyp of (bool * identifier located)
-  | TacDestructConcl
-  | TacSuperAuto of (int option * reference list * bool * bool)
-  | TacDAuto of int or_var option * int option * 'constr list
+  | TacTrivial of debug * 'constr list * string list option
+  | TacAuto of debug * int or_var option * 'constr list * string list option
 
   (* Context management *)
   | TacClear of bool * 'id list
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 5475daa8..08800902 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -72,14 +72,6 @@ let pf_get_new_ids ids gls =
     (fun id acc -> (next_ident_away id (acc@avoid))::acc)
     ids []
 
-let pf_interp_constr gls c =
-  let evc = project gls in
-  Constrintern.interp_constr evc (pf_env gls) c
-
-let pf_interp_type gls c =
-  let evc = project gls in
-  Constrintern.interp_type evc (pf_env gls) c
-
 let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id
 
 let pf_parse_const gls = compose (pf_global gls) id_of_string
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 884a0307..402002de 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -48,9 +48,6 @@ val pf_type_of            : goal sigma -> constr -> types
 val pf_check_type         : goal sigma -> constr -> types -> unit
 val pf_hnf_type_of        : goal sigma -> constr -> types
 
-val pf_interp_constr      : goal sigma -> Topconstr.constr_expr -> constr
-val pf_interp_type        : goal sigma -> Topconstr.constr_expr -> types
-
 val pf_get_hyp            : goal sigma -> identifier -> named_declaration
 val pf_get_hyp_typ        : goal sigma -> identifier -> types
 
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 1c2fb278..b23f361c 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -49,11 +49,12 @@ let db_pr_goal g =
 
 (* Prints the commands *)
 let help () =
-  msgnl (str "Commands: <Enter>=Continue" ++ fnl() ++
-         str "          h/?=Help" ++ fnl() ++
-         str "          r<num>=Run <num> times" ++ fnl() ++
-         str "          s=Skip" ++ fnl() ++
-         str "          x=Exit")
+  msgnl (str "Commands: <Enter> = Continue" ++ fnl() ++
+         str "          h/? = Help" ++ fnl() ++
+         str "          r <num> = Run <num> times" ++ fnl() ++
+         str "          r <string> = Run up to next idtac <string>" ++ fnl() ++
+         str "          s = Skip" ++ fnl() ++
+         str "          x = Exit")
 
 (* Prints the goal and the command to be executed *)
 let goal_com g tac =
@@ -62,37 +63,62 @@ let goal_com g tac =
     msg (str "Going to execute:" ++ fnl () ++ !prtac tac ++ fnl ())
   end
 
-(* Gives the number of a run command *)
+let skipped = ref 0
+let skip = ref 0
+let breakpoint = ref None
+
+let rec drop_spaces inst i =
+  if String.length inst > i && inst.[i] = ' ' then drop_spaces inst (i+1)
+  else i
+
+let possibly_unquote s =
+  if String.length s >= 2 & s.[0] = '"' & s.[String.length s - 1] = '"' then
+    String.sub s 1 (String.length s - 2)
+  else
+    s
+
+(* (Re-)initialize debugger *)
+let db_initialize () =
+  skip:=0;skipped:=0;breakpoint:=None
+
+(* Gives the number of steps or next breakpoint of a run command *)
 let run_com inst =
   if (String.get inst 0)='r' then
-    let num = int_of_string (String.sub inst 1 ((String.length inst)-1)) in
-    if num>0 then num
-    else raise (Invalid_argument "run_com")
+    let i = drop_spaces inst 1 in
+    if String.length inst > i then
+      let s = String.sub inst i (String.length inst - i) in
+      if inst.[0] >= '0' && inst.[0] <= '9' then
+        let num = int_of_string s in
+        if num<0 then raise (Invalid_argument "run_com");
+        skip:=num;skipped:=0
+      else
+        breakpoint:=Some (possibly_unquote s)
+    else
+      raise (Invalid_argument "run_com")
   else
     raise (Invalid_argument "run_com")
 
-let allskip = ref 0
-let skip = ref 0
-
 (* Prints the run counter *)
 let run ini =
   if not ini then
+  begin
     for i=1 to 2 do
       print_char (Char.chr 8);print_char (Char.chr 13)
     done;
-  msg (str "Executed expressions: " ++ int (!allskip - !skip) ++
-       fnl() ++ fnl())
+    msg (str "Executed expressions: " ++ int !skipped ++ fnl() ++ fnl())
+  end;
+  incr skipped
 
 (* Prints the prompt *)
 let rec prompt level =
   begin
     msg (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ");
     flush stdout;
-    let exit () = skip:=0;allskip:=0;raise Sys.Break in
+    let exit () = skip:=0;skipped:=0;raise Sys.Break in
     let inst = try read_line () with End_of_file -> exit () in
     match inst with
-    | ""  -> true
-    | "s" -> false
+    | ""  -> DebugOn (level+1)
+    | "s" -> DebugOff
     | "x" -> print_char (Char.chr 8); exit ()
     | "h"| "?" ->
       begin
@@ -100,32 +126,34 @@ let rec prompt level =
         prompt level
       end
     | _ ->
-      (try let ctr=run_com inst in skip:=ctr;allskip:=ctr;run true;true
+      (try run_com inst;run true;DebugOn (level+1)
        with Failure _ | Invalid_argument _ -> prompt level)
   end
 
 (* Prints the state and waits for an instruction *)
 let debug_prompt lev g tac f =
   (* What to print and to do next *)
-  let continue =
-    if !skip = 0 then (goal_com g tac; prompt lev)
-    else (decr skip; run false; if !skip=0 then allskip:=0; true) in
+  let newlevel =
+    if !skip = 0 then
+      if !breakpoint = None then (goal_com g tac; prompt lev)
+      else (run false; DebugOn (lev+1))
+    else (decr skip; run false; if !skip=0 then skipped:=0; DebugOn (lev+1)) in
   (* What to execute *)
-  try f (if continue then DebugOn (lev+1) else DebugOff)
+  try f newlevel
   with e ->
-    skip:=0; allskip:=0;
+    skip:=0; skipped:=0;
     if Logic.catchable_exception e then
       ppnl (str "Level " ++ int lev ++ str ": " ++ !explain_logic_error e);
     raise e
 
 (* Prints a constr *)
 let db_constr debug env c =
-  if debug <> DebugOff & !skip = 0 then
+  if debug <> DebugOff & !skip = 0 & !breakpoint = None then
     msgnl (str "Evaluated term: " ++ print_constr_env env c)
 
 (* Prints the pattern rule *)
 let db_pattern_rule debug num r =
-  if debug <> DebugOff & !skip = 0 then
+  if debug <> DebugOff & !skip = 0 & !breakpoint = None then
   begin
     msgnl (str "Pattern rule " ++ int num ++ str ":");
     msgnl (str "|" ++ spc () ++ !prmatchrl r)
@@ -138,38 +166,38 @@ let hyp_bound = function
 
 (* Prints a matched hypothesis *)
 let db_matched_hyp debug env (id,_,c) ido =
-  if debug <> DebugOff & !skip = 0 then
+  if debug <> DebugOff & !skip = 0 & !breakpoint = None then
     msgnl (str "Hypothesis " ++
            str ((Names.string_of_id id)^(hyp_bound ido)^
                 " has been matched: ") ++ print_constr_env env c)
 
 (* Prints the matched conclusion *)
 let db_matched_concl debug env c =
-  if debug <> DebugOff & !skip = 0 then
+  if debug <> DebugOff & !skip = 0 & !breakpoint = None then
     msgnl (str "Conclusion has been matched: " ++ print_constr_env env c)
 
 (* Prints a success message when the goal has been matched *)
 let db_mc_pattern_success debug =
-  if debug <> DebugOff & !skip = 0 then
+  if debug <> DebugOff & !skip = 0 & !breakpoint = None then
     msgnl (str "The goal has been successfully matched!" ++ fnl() ++
            str "Let us execute the right-hand side part..." ++ fnl())
 
 (* Prints a failure message for an hypothesis pattern *)
 let db_hyp_pattern_failure debug env (na,hyp) =
-  if debug <> DebugOff & !skip = 0 then
+  if debug <> DebugOff & !skip = 0 & !breakpoint = None then
     msgnl (str ("The pattern hypothesis"^(hyp_bound na)^
                 " cannot match: ") ++
            !prmatchpatt env hyp)
 
 (* Prints a matching failure message for a rule *)
 let db_matching_failure debug =
-  if debug <> DebugOff & !skip = 0 then
+  if debug <> DebugOff & !skip = 0 & !breakpoint = None then
     msgnl (str "This rule has failed due to matching errors!" ++ fnl() ++
            str "Let us try the next one...")
 
 (* Prints an evaluation failure message for a rule *)
 let db_eval_failure debug s =
-  if debug <> DebugOff & !skip = 0 then
+  if debug <> DebugOff & !skip = 0 & !breakpoint = None then
     let s = str "message \"" ++ s ++ str "\"" in
     msgnl
       (str "This rule has failed due to \"Fail\" tactic (" ++
@@ -177,9 +205,20 @@ let db_eval_failure debug s =
 
 (* Prints a logic failure message for a rule *)
 let db_logic_failure debug err =
-  if debug <> DebugOff & !skip = 0 then
+  if debug <> DebugOff & !skip = 0 & !breakpoint = None then
   begin
     msgnl (!explain_logic_error err);
     msgnl (str "This rule has failed due to a logic error!" ++ fnl() ++
            str "Let us try the next one...")
   end
+
+let is_breakpoint brkname s = match brkname, s with
+  | Some s, MsgString s'::_ -> s = s'
+  | _ -> false
+
+let db_breakpoint debug s =
+  match debug with
+  | DebugOn lev when s <> [] & is_breakpoint !breakpoint s ->
+      breakpoint:=None
+  | _ ->
+      ()
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index d96f4c74..62c2359b 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -34,6 +34,9 @@ type debug_info =
 val debug_prompt :
   int -> goal sigma -> glob_tactic_expr -> (debug_info -> 'a) -> 'a
 
+(** Initializes debugger *)
+val db_initialize : unit -> unit
+
 (** Prints a constr *)
 val db_constr : debug_info -> env -> constr -> unit
 
@@ -72,3 +75,7 @@ val explain_logic_error_no_anomaly : (exn -> Pp.std_ppcmds) ref
 
 (** Prints a logic failure message for a rule *)
 val db_logic_failure : debug_info -> exn -> unit
+
+(** Prints a logic failure message for a rule *)
+val db_breakpoint : debug_info ->
+  identifier Util.located message_token list -> unit