Adds a shelve tactic.

The shelve tactic puts all the focused goals out of sight. They can be later recalled by the Unshelve command.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17013 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 356 insertions, 235 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 3a00d76f0..6b847ec01 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -91,6 +91,8 @@ type proof = {
      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;
+  (* List of goals that have been shelved. *)
+  shelf : Goal.goal list;
 }
 
 (*** General proof functions ***)
@@ -107,7 +109,8 @@ let proof p =
   let stack =
     map_minus_one (fun (_,_,c) -> Proofview.focus_context c) p.focus_stack
   in
-  (goals,stack,sigma)
+  let shelf = p.shelf in
+  (goals,stack,shelf,sigma)
 
 let rec unroll_focus pv = function
   | (_,_,ctx)::stk -> unroll_focus (Proofview.unfocus ctx pv) stk
@@ -223,13 +226,16 @@ let unfocused = is_last_focus end_of_stack_kind
 let start goals =
   let pr = {
     proofview = Proofview.init goals ;
-    focus_stack = [] } in
+    focus_stack = [] ;
+    shelf = [] } in
   _focus end_of_stack (Obj.repr ()) 1 (List.length goals) pr
 
 exception UnfinishedProof
+exception HasShelvedGoals
 exception HasUnresolvedEvar
 let _ = Errors.register_handler begin function
   | UnfinishedProof -> Errors.error "Some goals have not been solved."
+  | HasShelvedGoals -> Errors.error "Some goals have been left on the shelf."
   | HasUnresolvedEvar -> Errors.error "Some existential variables are uninstantiated."
   | _ -> raise Errors.Unhandled
 end
@@ -237,6 +243,8 @@ end
 let return p =
   if not (is_done p) then
     raise UnfinishedProof
+  else if not (CList.is_empty (p.shelf)) then
+    raise HasShelvedGoals
   else if has_unresolved_evar p then
     (* spiwack: for compatibility with <= 8.3 proof engine *)
     raise HasUnresolvedEvar
@@ -252,8 +260,18 @@ let initial_goals p = Proofview.initial_goals p.proofview
 
 let run_tactic env tac pr =
   let sp = pr.proofview in
-  let (_,tacticced_proofview,status) = Proofview.apply env tac sp in
-  { pr with proofview = tacticced_proofview },status
+  let (_,tacticced_proofview,(status,to_shelve)) = Proofview.apply env tac sp in
+  let shelf =
+    let pre_shelf = pr.shelf@to_shelve in
+    (* Compacting immediately: if someone shelves a goal, he probably
+       expects to solve it soon. *)
+    Proofview.in_proofview tacticced_proofview begin fun sigma ->
+      Option.List.flatten begin
+        List.map (fun g -> Goal.advance sigma g) pre_shelf
+      end
+    end
+  in
+  { pr with proofview = tacticced_proofview ; shelf },status
 
 let emit_side_effects eff pr =
   {pr with proofview = Proofview.emit_side_effects eff pr.proofview}
@@ -262,6 +280,11 @@ let emit_side_effects eff pr =
 
 let in_proof p k = Proofview.in_proofview p.proofview k
 
+(* 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 =
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 66aee0313..0df55759d 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -40,9 +40,14 @@ type proof
    functions to ide-s. This would be better than spawning a new nearly
    identical function everytime. Hence the generic name. *)
 (* In this version: returns the focused goals, a representation of the
-   focus stack (the number of goals at each level) and the underlying
+   focus stack (the goals at each level), a representation
+   of the shelf (the list of goals on the shelf),and the underlying
    evar_map *)
-val proof : proof -> Goal.goal list * (Goal.goal list * Goal.goal list) list * Evd.evar_map
+val proof : proof ->
+  Goal.goal list
+  * (Goal.goal list * Goal.goal list) list
+  * Goal.goal list
+  * Evd.evar_map
 
 (*** General proof functions ***)
 
@@ -58,8 +63,10 @@ val partial_proof : proof -> Term.constr list
 
 (* 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.
     Raises [HasUnresolvedEvar] if some evars have been left undefined. *)
 exception UnfinishedProof
+exception HasShelvedGoals
 exception HasUnresolvedEvar
 val return : proof -> Evd.evar_map
 
@@ -140,6 +147,10 @@ val maximal_unfocus : 'a focus_kind -> proof -> proof
 
 val in_proof : proof -> (Evd.evar_map -> 'a) -> 'a
 
+(* Remove all the goals from the shelf and adds them at the end of the
+   focused goals. *)
+val unshelve : proof -> proof
+
 (*** Compatibility layer with <=v8.2 ***)
 module V82 : sig
   val subgoals : proof -> Goal.goal list Evd.sigma
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 2ca95d958..3c0e29023 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -262,10 +262,11 @@ let set_used_variables l =
       pstates := { p with section_vars = Some ctx} :: rest
 
 let get_open_goals () =
-  let gl, gll, _ = Proof.proof (cur_pstate ()).proof in
+  let gl, gll, shelf , _ = Proof.proof (cur_pstate ()).proof in
   List.length gl +
   List.fold_left (+) 0
-    (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll)
+    (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) +
+  List.length shelf
 
 type closed_proof =
   Names.Id.t *
@@ -293,6 +294,9 @@ let return_proof () =
    | Proof.UnfinishedProof ->
        raise (Errors.UserError("last tactic before Qed",
          str"Attempt to save an incomplete proof"))
+   | Proof.HasShelvedGoals ->
+       raise (Errors.UserError("last tactic before Qed",
+         str"Attempt to save a proof with shelved goals"))
    | Proof.HasUnresolvedEvar ->
        raise (Errors.UserError("last tactic before Qed",
          str"Attempt to save a proof with existential " ++
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index bb1d5758d..5e1e1e6a4 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -565,7 +565,21 @@ let tclTIMEOUT n t =
     | Util.Inr e -> tclZERO e
 
 let mark_as_unsafe =
-  Proof.put false
+  Proof.put (false,[])
+
+(* Shelves all the goals under focus. *)
+let shelve =
+  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+  let (>>=) = Proof.bind in
+  let (>>) = Proof.seq in
+  Proof.get >>= fun initial ->
+  Proof.set {initial with comb=[]} >>
+  Proof.put (true,initial.comb)
+
+(* [unshelve l p] adds all the goals in [l] at the end of the focused
+   goals of p *)
+let unshelve l p =
+  { p with comb = p.comb@l }
 
 (*** Commands ***)
 
@@ -690,7 +704,7 @@ module V82 = struct
     with Proof_errors.TacticFailure e -> raise e
 
   let put_status b =
-    Proof.put b
+    Proof.put (b,[])
 
   let catchable_exception = catchable_exception
 end
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 5b25c003d..c483cd371 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -120,7 +120,7 @@ type +'a tactic
 (* Applies a tactic to the current proofview. *)
 (* the return boolean signals the use of an unsafe tactic, in which
    case it is [false]. *)
-val apply : Environ.env -> 'a tactic -> proofview -> 'a * proofview * bool
+val apply : Environ.env -> 'a tactic -> proofview -> 'a * proofview * (bool*Goal.goal list)
 
 (*** tacticals ***)
 
@@ -210,6 +210,14 @@ val tclEVARMAP : Evd.evar_map tactic
    environment is returned by {!Proofview.Goal.env}. *)
 val tclENV : Environ.env tactic
 
+(* Shelves all the goals under focus. The goals are placed on the
+   shelf for later use (or being solved by side-effects). *)
+val shelve : unit tactic
+
+(* [unshelve l p] adds all the goals in [l] at the end of the focused
+   goals of p *)
+val unshelve : Goal.goal list -> proofview -> proofview
+
 exception Timeout
 (** [tclTIMEOUT n t] can have only one success.
     In case of timeout if fails with [tclZERO Timeout]. *)
diff --git a/proofs/proofview_gen.ml b/proofs/proofview_gen.ml
index 0f9d38775..b813eabaa 100644
--- a/proofs/proofview_gen.ml
+++ b/proofs/proofview_gen.ml
@@ -101,7 +101,7 @@ type proofview = { initial : (Term.constr*Term.types)
 
 type logicalState = proofview
 
-type logicalMessageType = bool
+type logicalMessageType = bool*Goal.goal list
 
 type logicalEnvironment = Environ.env
 
@@ -187,28 +187,30 @@ module Logical =
  struct 
   type 'a t =
     __ -> ('a -> proofview -> __ -> (__ -> __
-    -> (__ -> bool -> __ -> (__ -> (exn -> __
-    IOBase.coq_T) -> __ IOBase.coq_T) -> (exn
-    -> __ IOBase.coq_T) -> __ IOBase.coq_T)
-    -> __ -> (__ -> (exn -> __ IOBase.coq_T)
-    -> __ IOBase.coq_T) -> (exn -> __
-    IOBase.coq_T) -> __ IOBase.coq_T) ->
-    Environ.env -> __ -> (__ -> bool -> __ ->
+    -> (__ -> (bool*Goal.goal list) -> __ ->
     (__ -> (exn -> __ IOBase.coq_T) -> __
     IOBase.coq_T) -> (exn -> __ IOBase.coq_T)
     -> __ IOBase.coq_T) -> __ -> (__ -> (exn
     -> __ IOBase.coq_T) -> __ IOBase.coq_T)
     -> (exn -> __ IOBase.coq_T) -> __
-    IOBase.coq_T) -> proofview -> __ -> (__
-    -> __ -> (__ -> bool -> __ -> (__ -> (exn
+    IOBase.coq_T) -> Environ.env -> __ -> (__
+    -> (bool*Goal.goal list) -> __ -> (__ ->
+    (exn -> __ IOBase.coq_T) -> __
+    IOBase.coq_T) -> (exn -> __ IOBase.coq_T)
+    -> __ IOBase.coq_T) -> __ -> (__ -> (exn
     -> __ IOBase.coq_T) -> __ IOBase.coq_T)
     -> (exn -> __ IOBase.coq_T) -> __
-    IOBase.coq_T) -> __ -> (__ -> (exn -> __
-    IOBase.coq_T) -> __ IOBase.coq_T) -> (exn
-    -> __ IOBase.coq_T) -> __ IOBase.coq_T)
-    -> Environ.env -> __ -> (__ -> bool -> __
+    IOBase.coq_T) -> proofview -> __ -> (__
+    -> __ -> (__ -> (bool*Goal.goal list) ->
+    __ -> (__ -> (exn -> __ IOBase.coq_T) ->
+    __ IOBase.coq_T) -> (exn -> __
+    IOBase.coq_T) -> __ IOBase.coq_T) -> __
     -> (__ -> (exn -> __ IOBase.coq_T) -> __
     IOBase.coq_T) -> (exn -> __ IOBase.coq_T)
+    -> __ IOBase.coq_T) -> Environ.env -> __
+    -> (__ -> (bool*Goal.goal list) -> __ ->
+    (__ -> (exn -> __ IOBase.coq_T) -> __
+    IOBase.coq_T) -> (exn -> __ IOBase.coq_T)
     -> __ IOBase.coq_T) -> __ -> (__ -> (exn
     -> __ IOBase.coq_T) -> __ IOBase.coq_T)
     -> (exn -> __ IOBase.coq_T) -> __
@@ -216,35 +218,37 @@ module Logical =
   
   (** val ret :
       'a1 -> __ -> ('a1 -> proofview -> __ ->
-      ('a2 -> __ -> (__ -> bool -> __ -> (__
-      -> (exn -> __ IOBase.coq_T) -> __
+      ('a2 -> __ -> (__ -> (bool*Goal.goal
+      list) -> __ -> (__ -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) ->
+      (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> __ -> (__ -> (exn ->
+      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+      (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> Environ.env -> __ ->
+      (__ -> (bool*Goal.goal list) -> __ ->
+      (__ -> (exn -> __ IOBase.coq_T) -> __
       IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) -> __
       -> (__ -> (exn -> __ IOBase.coq_T) ->
       __ IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> (__ -> bool -> __
-      -> (__ -> (exn -> __ IOBase.coq_T) ->
-      __ IOBase.coq_T) -> (exn -> __
+      proofview -> __ -> ('a2 -> __ -> ('a3
+      -> (bool*Goal.goal list) -> __ -> (__
+      -> (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) -> __
       -> (__ -> (exn -> __ IOBase.coq_T) ->
       __ IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
-      proofview -> __ -> ('a2 -> __ -> ('a3
-      -> bool -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) ->
+      Environ.env -> __ -> ('a3 ->
+      (bool*Goal.goal list) -> __ -> ('a4 ->
       (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> Environ.env -> __ ->
-      ('a3 -> bool -> __ -> ('a4 -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> ('a4 -> (exn ->
-      'a5 IOBase.coq_T) -> 'a5 IOBase.coq_T)
-      -> (exn -> 'a5 IOBase.coq_T) -> 'a5
-      IOBase.coq_T **)
+      IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) -> __
+      -> ('a4 -> (exn -> 'a5 IOBase.coq_T) ->
+      'a5 IOBase.coq_T) -> (exn -> 'a5
+      IOBase.coq_T) -> 'a5 IOBase.coq_T **)
   
   let ret x =
     (); (fun _ k s -> Obj.magic k x s)
@@ -252,30 +256,33 @@ module Logical =
   (** val bind :
       'a1 t -> ('a1 -> 'a2 t) -> __ -> ('a2
       -> proofview -> __ -> ('a3 -> __ -> (__
-      -> bool -> __ -> (__ -> (exn -> __
+      -> (bool*Goal.goal list) -> __ -> (__
+      -> (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) -> __
+      -> (__ -> (exn -> __ IOBase.coq_T) ->
+      __ IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
+      Environ.env -> __ -> (__ ->
+      (bool*Goal.goal list) -> __ -> (__ ->
       (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> Environ.env -> __ ->
-      (__ -> bool -> __ -> (__ -> (exn -> __
+      IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) -> __
+      -> (__ -> (exn -> __ IOBase.coq_T) ->
+      __ IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
-      (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> proofview -> __ ->
-      ('a3 -> __ -> ('a4 -> bool -> __ -> (__
+      proofview -> __ -> ('a3 -> __ -> ('a4
+      -> (bool*Goal.goal list) -> __ -> (__
       -> (exn -> __ IOBase.coq_T) -> __
       IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) -> __
       -> (__ -> (exn -> __ IOBase.coq_T) ->
       __ IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> ('a4 -> bool -> __
-      -> ('a5 -> (exn -> __ IOBase.coq_T) ->
-      __ IOBase.coq_T) -> (exn -> __
+      Environ.env -> __ -> ('a4 ->
+      (bool*Goal.goal list) -> __ -> ('a5 ->
+      (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) -> __
       -> ('a5 -> (exn -> 'a6 IOBase.coq_T) ->
       'a6 IOBase.coq_T) -> (exn -> 'a6
@@ -288,35 +295,37 @@ module Logical =
   
   (** val ignore :
       'a1 t -> __ -> (unit -> proofview -> __
-      -> ('a2 -> __ -> (__ -> bool -> __ ->
+      -> ('a2 -> __ -> (__ -> (bool*Goal.goal
+      list) -> __ -> (__ -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) ->
+      (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> __ -> (__ -> (exn ->
+      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+      (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> Environ.env -> __ ->
+      (__ -> (bool*Goal.goal list) -> __ ->
       (__ -> (exn -> __ IOBase.coq_T) -> __
       IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) -> __
       -> (__ -> (exn -> __ IOBase.coq_T) ->
       __ IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> (__ -> bool -> __
-      -> (__ -> (exn -> __ IOBase.coq_T) ->
-      __ IOBase.coq_T) -> (exn -> __
+      proofview -> __ -> ('a2 -> __ -> ('a3
+      -> (bool*Goal.goal list) -> __ -> (__
+      -> (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) -> __
       -> (__ -> (exn -> __ IOBase.coq_T) ->
       __ IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
-      proofview -> __ -> ('a2 -> __ -> ('a3
-      -> bool -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) ->
-      (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+      Environ.env -> __ -> ('a3 ->
+      (bool*Goal.goal list) -> __ -> ('a4 ->
       (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> Environ.env -> __ ->
-      ('a3 -> bool -> __ -> ('a4 -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> ('a4 -> (exn ->
-      'a5 IOBase.coq_T) -> 'a5 IOBase.coq_T)
-      -> (exn -> 'a5 IOBase.coq_T) -> 'a5
-      IOBase.coq_T **)
+      IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) -> __
+      -> ('a4 -> (exn -> 'a5 IOBase.coq_T) ->
+      'a5 IOBase.coq_T) -> (exn -> 'a5
+      IOBase.coq_T) -> 'a5 IOBase.coq_T **)
   
   let ignore x =
     (); (fun _ k s ->
@@ -325,30 +334,33 @@ module Logical =
   (** val seq :
       unit t -> 'a1 t -> __ -> ('a1 ->
       proofview -> __ -> ('a2 -> __ -> (__ ->
-      bool -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) ->
+      (bool*Goal.goal list) -> __ -> (__ ->
       (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> Environ.env -> __ ->
-      (__ -> bool -> __ -> (__ -> (exn -> __
+      IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) -> __
+      -> (__ -> (exn -> __ IOBase.coq_T) ->
+      __ IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
+      Environ.env -> __ -> (__ ->
+      (bool*Goal.goal list) -> __ -> (__ ->
       (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> proofview -> __ ->
-      ('a2 -> __ -> ('a3 -> bool -> __ -> (__
-      -> (exn -> __ IOBase.coq_T) -> __
       IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) -> __
       -> (__ -> (exn -> __ IOBase.coq_T) ->
       __ IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> ('a3 -> bool -> __
-      -> ('a4 -> (exn -> __ IOBase.coq_T) ->
+      proofview -> __ -> ('a2 -> __ -> ('a3
+      -> (bool*Goal.goal list) -> __ -> (__
+      -> (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) -> __
+      -> (__ -> (exn -> __ IOBase.coq_T) ->
       __ IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) ->
+      Environ.env -> __ -> ('a3 ->
+      (bool*Goal.goal list) -> __ -> ('a4 ->
+      (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) -> __
       -> ('a4 -> (exn -> 'a5 IOBase.coq_T) ->
       'a5 IOBase.coq_T) -> (exn -> 'a5
@@ -362,30 +374,33 @@ module Logical =
   (** val set :
       logicalState -> __ -> (unit ->
       proofview -> __ -> ('a1 -> __ -> (__ ->
-      bool -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) ->
-      (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+      (bool*Goal.goal list) -> __ -> (__ ->
       (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> Environ.env -> __ ->
-      (__ -> bool -> __ -> (__ -> (exn -> __
+      IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) -> __
+      -> (__ -> (exn -> __ IOBase.coq_T) ->
+      __ IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
+      Environ.env -> __ -> (__ ->
+      (bool*Goal.goal list) -> __ -> (__ ->
       (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> proofview -> __ ->
-      ('a1 -> __ -> ('a2 -> bool -> __ -> (__
-      -> (exn -> __ IOBase.coq_T) -> __
       IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) -> __
       -> (__ -> (exn -> __ IOBase.coq_T) ->
       __ IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> ('a2 -> bool -> __
-      -> ('a3 -> (exn -> __ IOBase.coq_T) ->
+      proofview -> __ -> ('a1 -> __ -> ('a2
+      -> (bool*Goal.goal list) -> __ -> (__
+      -> (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) -> __
+      -> (__ -> (exn -> __ IOBase.coq_T) ->
       __ IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) ->
+      Environ.env -> __ -> ('a2 ->
+      (bool*Goal.goal list) -> __ -> ('a3 ->
+      (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) -> __
       -> ('a3 -> (exn -> 'a4 IOBase.coq_T) ->
       'a4 IOBase.coq_T) -> (exn -> 'a4
@@ -396,35 +411,37 @@ module Logical =
   
   (** val get :
       __ -> (logicalState -> proofview -> __
-      -> ('a1 -> __ -> (__ -> bool -> __ ->
+      -> ('a1 -> __ -> (__ -> (bool*Goal.goal
+      list) -> __ -> (__ -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) ->
+      (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> __ -> (__ -> (exn ->
+      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+      (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> Environ.env -> __ ->
+      (__ -> (bool*Goal.goal list) -> __ ->
       (__ -> (exn -> __ IOBase.coq_T) -> __
       IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) -> __
       -> (__ -> (exn -> __ IOBase.coq_T) ->
       __ IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> (__ -> bool -> __
-      -> (__ -> (exn -> __ IOBase.coq_T) ->
-      __ IOBase.coq_T) -> (exn -> __
+      proofview -> __ -> ('a1 -> __ -> ('a2
+      -> (bool*Goal.goal list) -> __ -> (__
+      -> (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) -> __
       -> (__ -> (exn -> __ IOBase.coq_T) ->
       __ IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
-      proofview -> __ -> ('a1 -> __ -> ('a2
-      -> bool -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) ->
-      (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+      Environ.env -> __ -> ('a2 ->
+      (bool*Goal.goal list) -> __ -> ('a3 ->
       (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> Environ.env -> __ ->
-      ('a2 -> bool -> __ -> ('a3 -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> ('a3 -> (exn ->
-      'a4 IOBase.coq_T) -> 'a4 IOBase.coq_T)
-      -> (exn -> 'a4 IOBase.coq_T) -> 'a4
-      IOBase.coq_T **)
+      IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) -> __
+      -> ('a3 -> (exn -> 'a4 IOBase.coq_T) ->
+      'a4 IOBase.coq_T) -> (exn -> 'a4
+      IOBase.coq_T) -> 'a4 IOBase.coq_T **)
   
   let get r k s =
     Obj.magic k s s
@@ -432,30 +449,33 @@ module Logical =
   (** val put :
       logicalMessageType -> __ -> (unit ->
       proofview -> __ -> ('a1 -> __ -> (__ ->
-      bool -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) ->
+      (bool*Goal.goal list) -> __ -> (__ ->
       (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> Environ.env -> __ ->
-      (__ -> bool -> __ -> (__ -> (exn -> __
+      IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) -> __
+      -> (__ -> (exn -> __ IOBase.coq_T) ->
+      __ IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
+      Environ.env -> __ -> (__ ->
+      (bool*Goal.goal list) -> __ -> (__ ->
       (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> proofview -> __ ->
-      ('a1 -> __ -> ('a2 -> bool -> __ -> (__
-      -> (exn -> __ IOBase.coq_T) -> __
       IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) -> __
       -> (__ -> (exn -> __ IOBase.coq_T) ->
       __ IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> ('a2 -> bool -> __
-      -> ('a3 -> (exn -> __ IOBase.coq_T) ->
+      proofview -> __ -> ('a1 -> __ -> ('a2
+      -> (bool*Goal.goal list) -> __ -> (__
+      -> (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) -> __
+      -> (__ -> (exn -> __ IOBase.coq_T) ->
       __ IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) ->
+      Environ.env -> __ -> ('a2 ->
+      (bool*Goal.goal list) -> __ -> ('a3 ->
+      (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) -> __
       -> ('a3 -> (exn -> 'a4 IOBase.coq_T) ->
       'a4 IOBase.coq_T) -> (exn -> 'a4
@@ -465,74 +485,81 @@ module Logical =
     (); (fun _ k s _ k0 e _ k1 ->
       Obj.magic k () s __ k0 e __
         (fun b c' ->
-        k1 b (if m then c' else false)))
+        k1 b
+          ((if fst m then fst c' else false),
+          (List.append (snd m) (snd c')))))
   
   (** val current :
       __ -> (logicalEnvironment -> proofview
-      -> __ -> ('a1 -> __ -> (__ -> bool ->
-      __ -> (__ -> (exn -> __ IOBase.coq_T)
-      -> __ IOBase.coq_T) -> (exn -> __
+      -> __ -> ('a1 -> __ -> (__ ->
+      (bool*Goal.goal list) -> __ -> (__ ->
+      (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) -> __
       -> (__ -> (exn -> __ IOBase.coq_T) ->
       __ IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> (__ -> bool -> __
-      -> (__ -> (exn -> __ IOBase.coq_T) ->
-      __ IOBase.coq_T) -> (exn -> __
+      Environ.env -> __ -> (__ ->
+      (bool*Goal.goal list) -> __ -> (__ ->
+      (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) -> __
       -> (__ -> (exn -> __ IOBase.coq_T) ->
       __ IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
       proofview -> __ -> ('a1 -> __ -> ('a2
-      -> bool -> __ -> (__ -> (exn -> __
+      -> (bool*Goal.goal list) -> __ -> (__
+      -> (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) -> __
+      -> (__ -> (exn -> __ IOBase.coq_T) ->
+      __ IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
+      Environ.env -> __ -> ('a2 ->
+      (bool*Goal.goal list) -> __ -> ('a3 ->
       (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> Environ.env -> __ ->
-      ('a2 -> bool -> __ -> ('a3 -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> ('a3 -> (exn ->
-      'a4 IOBase.coq_T) -> 'a4 IOBase.coq_T)
-      -> (exn -> 'a4 IOBase.coq_T) -> 'a4
-      IOBase.coq_T **)
+      IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) -> __
+      -> ('a3 -> (exn -> 'a4 IOBase.coq_T) ->
+      'a4 IOBase.coq_T) -> (exn -> 'a4
+      IOBase.coq_T) -> 'a4 IOBase.coq_T **)
   
   let current r k s r0 k0 e =
     Obj.magic k e s __ k0 e
   
   (** val zero :
       exn -> __ -> ('a1 -> proofview -> __ ->
-      ('a2 -> __ -> (__ -> bool -> __ -> (__
-      -> (exn -> __ IOBase.coq_T) -> __
+      ('a2 -> __ -> (__ -> (bool*Goal.goal
+      list) -> __ -> (__ -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) ->
+      (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> __ -> (__ -> (exn ->
+      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+      (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> Environ.env -> __ ->
+      (__ -> (bool*Goal.goal list) -> __ ->
+      (__ -> (exn -> __ IOBase.coq_T) -> __
       IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) -> __
       -> (__ -> (exn -> __ IOBase.coq_T) ->
       __ IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> (__ -> bool -> __
-      -> (__ -> (exn -> __ IOBase.coq_T) ->
-      __ IOBase.coq_T) -> (exn -> __
+      proofview -> __ -> ('a2 -> __ -> ('a3
+      -> (bool*Goal.goal list) -> __ -> (__
+      -> (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) -> __
       -> (__ -> (exn -> __ IOBase.coq_T) ->
       __ IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
-      proofview -> __ -> ('a2 -> __ -> ('a3
-      -> bool -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) ->
-      (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> Environ.env -> __ ->
-      ('a3 -> bool -> __ -> ('a4 -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+      Environ.env -> __ -> ('a3 ->
+      (bool*Goal.goal list) -> __ -> ('a4 ->
       (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> ('a4 -> (exn ->
-      'a5 IOBase.coq_T) -> 'a5 IOBase.coq_T)
-      -> (exn -> 'a5 IOBase.coq_T) -> 'a5
-      IOBase.coq_T **)
+      IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) -> __
+      -> ('a4 -> (exn -> 'a5 IOBase.coq_T) ->
+      'a5 IOBase.coq_T) -> (exn -> 'a5
+      IOBase.coq_T) -> 'a5 IOBase.coq_T **)
   
   let zero e =
     (); (fun _ k s _ k0 e0 _ k1 _ sk fk ->
@@ -541,30 +568,33 @@ module Logical =
   (** val plus :
       'a1 t -> (exn -> 'a1 t) -> __ -> ('a1
       -> proofview -> __ -> ('a2 -> __ -> (__
-      -> bool -> __ -> (__ -> (exn -> __
+      -> (bool*Goal.goal list) -> __ -> (__
+      -> (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) -> __
+      -> (__ -> (exn -> __ IOBase.coq_T) ->
+      __ IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
+      Environ.env -> __ -> (__ ->
+      (bool*Goal.goal list) -> __ -> (__ ->
       (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> Environ.env -> __ ->
-      (__ -> bool -> __ -> (__ -> (exn -> __
+      IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) -> __
+      -> (__ -> (exn -> __ IOBase.coq_T) ->
+      __ IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
-      (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> proofview -> __ ->
-      ('a2 -> __ -> ('a3 -> bool -> __ -> (__
+      proofview -> __ -> ('a2 -> __ -> ('a3
+      -> (bool*Goal.goal list) -> __ -> (__
       -> (exn -> __ IOBase.coq_T) -> __
       IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) -> __
       -> (__ -> (exn -> __ IOBase.coq_T) ->
       __ IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> ('a3 -> bool -> __
-      -> ('a4 -> (exn -> __ IOBase.coq_T) ->
-      __ IOBase.coq_T) -> (exn -> __
+      Environ.env -> __ -> ('a3 ->
+      (bool*Goal.goal list) -> __ -> ('a4 ->
+      (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) -> __
       -> ('a4 -> (exn -> 'a5 IOBase.coq_T) ->
       'a5 IOBase.coq_T) -> (exn -> 'a5
@@ -580,30 +610,33 @@ module Logical =
   (** val split :
       'a1 t -> __ -> (('a1, exn -> 'a1 t)
       list_view -> proofview -> __ -> ('a2 ->
-      __ -> (__ -> bool -> __ -> (__ -> (exn
-      -> __ IOBase.coq_T) -> __ IOBase.coq_T)
-      -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> Environ.env -> __ ->
-      (__ -> bool -> __ -> (__ -> (exn -> __
+      __ -> (__ -> (bool*Goal.goal list) ->
+      __ -> (__ -> (exn -> __ IOBase.coq_T)
+      -> __ IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) -> __
+      -> (__ -> (exn -> __ IOBase.coq_T) ->
+      __ IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
+      Environ.env -> __ -> (__ ->
+      (bool*Goal.goal list) -> __ -> (__ ->
       (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> proofview -> __ ->
-      ('a2 -> __ -> ('a3 -> bool -> __ -> (__
-      -> (exn -> __ IOBase.coq_T) -> __
       IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) -> __
       -> (__ -> (exn -> __ IOBase.coq_T) ->
       __ IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> ('a3 -> bool -> __
-      -> ('a4 -> (exn -> __ IOBase.coq_T) ->
+      proofview -> __ -> ('a2 -> __ -> ('a3
+      -> (bool*Goal.goal list) -> __ -> (__
+      -> (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) -> __
+      -> (__ -> (exn -> __ IOBase.coq_T) ->
       __ IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) ->
+      Environ.env -> __ -> ('a3 ->
+      (bool*Goal.goal list) -> __ -> ('a4 ->
+      (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) -> __
       -> ('a4 -> (exn -> 'a5 IOBase.coq_T) ->
       'a5 IOBase.coq_T) -> (exn -> 'a5
@@ -614,7 +647,7 @@ module Logical =
       IOBase.bind
         (Obj.magic x __ (fun a s' _ k2 e0 ->
           k2 (a,s')) s __ (fun a _ k2 ->
-          k2 a true) e __
+          k2 a (true,[])) e __
           (fun a c _ sk0 fk0 ->
           sk0 (a,c) fk0) __ (fun a fk0 ->
           IOBase.ret (Cons (a,
@@ -629,8 +662,16 @@ module Logical =
         (fun x0 ->
         match x0 with
         | Nil exc ->
+          let c = true,[] in
           Obj.magic k (Nil exc) s __ k0 e __
-            (fun b c' -> k1 b c') __ sk fk
+            (fun b c' ->
+            k1 b
+              ((if fst c
+                then fst c'
+                else false),(List.append
+                              (snd c)
+                              (snd c')))) __
+            sk fk
         | Cons (p, y) ->
           let p0,m' = p in
           let a',s' = p0 in
@@ -642,39 +683,51 @@ module Logical =
               k2 a1 s'0 __ k3 e0 __
                 (fun b c' ->
                 k4 b
-                  (if c then c' else false))
+                  ((if fst c
+                    then fst c'
+                    else false),(List.append
+                                  (snd c)
+                                  (snd c'))))
                 __ sk0 fk1) fk0))) s' __ k0 e
             __ (fun b c' ->
-            k1 b (if m' then c' else false))
-            __ sk fk))
+            k1 b
+              ((if fst m'
+                then fst c'
+                else false),(List.append
+                              (snd m')
+                              (snd c')))) __
+            sk fk))
   
   (** val lift :
       'a1 NonLogical.t -> __ -> ('a1 ->
       proofview -> __ -> ('a2 -> __ -> (__ ->
-      bool -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) ->
-      (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+      (bool*Goal.goal list) -> __ -> (__ ->
       (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> Environ.env -> __ ->
-      (__ -> bool -> __ -> (__ -> (exn -> __
+      IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) -> __
+      -> (__ -> (exn -> __ IOBase.coq_T) ->
+      __ IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
+      Environ.env -> __ -> (__ ->
+      (bool*Goal.goal list) -> __ -> (__ ->
       (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> proofview -> __ ->
-      ('a2 -> __ -> ('a3 -> bool -> __ -> (__
-      -> (exn -> __ IOBase.coq_T) -> __
       IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) -> __
       -> (__ -> (exn -> __ IOBase.coq_T) ->
       __ IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> ('a3 -> bool -> __
-      -> ('a4 -> (exn -> __ IOBase.coq_T) ->
+      proofview -> __ -> ('a2 -> __ -> ('a3
+      -> (bool*Goal.goal list) -> __ -> (__
+      -> (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) -> __
+      -> (__ -> (exn -> __ IOBase.coq_T) ->
       __ IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) ->
+      Environ.env -> __ -> ('a3 ->
+      (bool*Goal.goal list) -> __ -> ('a4 ->
+      (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) -> __
       -> ('a4 -> (exn -> 'a5 IOBase.coq_T) ->
       'a5 IOBase.coq_T) -> (exn -> 'a5
@@ -684,7 +737,14 @@ module Logical =
     (); (fun _ k s _ k0 e _ k1 _ sk fk ->
       IOBase.bind x (fun x0 ->
         Obj.magic k x0 s __ k0 e __
-          (fun b c' -> k1 b c') __ sk fk))
+          (fun b c' ->
+          k1 b
+            ((if fst (true,[])
+              then fst c'
+              else false),(List.append
+                            (snd (true,[]))
+                            (snd c')))) __ sk
+          fk))
   
   (** val run :
       'a1 t -> logicalEnvironment ->
@@ -694,10 +754,10 @@ module Logical =
   
   let run x e s =
     Obj.magic x __ (fun a s' _ k e0 ->
-      k (a,s')) s __ (fun a _ k -> k a true)
-      e __ (fun a c _ sk fk -> sk (a,c) fk)
-      __ (fun a x0 -> IOBase.ret a)
-      (fun e0 ->
+      k (a,s')) s __ (fun a _ k ->
+      k a (true,[])) e __ (fun a c _ sk fk ->
+      sk (a,c) fk) __ (fun a x0 ->
+      IOBase.ret a) (fun e0 ->
       IOBase.raise
         ((fun e -> Proof_errors.TacticFailure e)
           e0))
diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli
index f9854ae0c..c1f1b5ee1 100644
--- a/proofs/proofview_monad.mli
+++ b/proofs/proofview_monad.mli
@@ -12,7 +12,8 @@ type logicalState = proofview
 
 type logicalEnvironment = Environ.env
 
-type logicalMessageType = bool
+(** status (safe/unsafe) * shelved goals *)
+type logicalMessageType = bool * Goal.goal list