Adds a tactic give_up.

Gives up on the focused goals. Shows an unsafe status. Unlike the admit tactic, the proof cannot be closed until the users goes back and solves these goals.

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

7 files changed, 371 insertions, 293 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 6b847ec01e..99654ab75f 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -93,6 +93,8 @@ type proof = {
   focus_stack: (_focus_condition*focus_info*Proofview.focus_context) list;
   (* List of goals that have been shelved. *)
   shelf : Goal.goal list;
+  (* List of goals that have been given up *)
+  given_up : Goal.goal list;
 }
 
 (*** General proof functions ***)
@@ -110,7 +112,8 @@ let proof p =
     map_minus_one (fun (_,_,c) -> Proofview.focus_context c) p.focus_stack
   in
   let shelf = p.shelf in
-  (goals,stack,shelf,sigma)
+  let given_up = p.given_up in
+  (goals,stack,shelf,given_up,sigma)
 
 let rec unroll_focus pv = function
   | (_,_,ctx)::stk -> unroll_focus (Proofview.unfocus ctx pv) stk
@@ -227,15 +230,18 @@ let start goals =
   let pr = {
     proofview = Proofview.init goals ;
     focus_stack = [] ;
-    shelf = [] } in
+    shelf = [] ;
+    given_up = [] } in
   _focus end_of_stack (Obj.repr ()) 1 (List.length goals) pr
 
 exception UnfinishedProof
 exception HasShelvedGoals
+exception HasGivenUpGoals
 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."
+  | HasGivenUpGoals -> Errors.error "Some goals have been given up."
   | HasUnresolvedEvar -> Errors.error "Some existential variables are uninstantiated."
   | _ -> raise Errors.Unhandled
 end
@@ -245,6 +251,8 @@ let return p =
     raise UnfinishedProof
   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
@@ -260,7 +268,7 @@ let initial_goals p = Proofview.initial_goals p.proofview
 
 let run_tactic env tac pr =
   let sp = pr.proofview in
-  let (_,tacticced_proofview,(status,to_shelve)) = Proofview.apply env tac sp in
+  let (_,tacticced_proofview,(status,(to_shelve,give_up))) = 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
@@ -271,7 +279,8 @@ let run_tactic env tac pr =
       end
     end
   in
-  { pr with proofview = tacticced_proofview ; shelf },status
+  let given_up = pr.given_up@give_up in
+  { pr with proofview = tacticced_proofview ; shelf ; given_up },status
 
 let emit_side_effects eff pr =
   {pr with proofview = Proofview.emit_side_effects eff pr.proofview}
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 0df55759db..4f7a242d30 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -40,13 +40,15 @@ 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 goals at each level), a representation
-   of the shelf (the list of goals on the shelf),and the underlying
+   focus stack (the goals at each level), a representation of the
+   shelf (the list of goals on the shelf), a representation of the
+   given up goals (the list of the given up goals) and the underlying
    evar_map *)
 val proof : proof ->
   Goal.goal list
   * (Goal.goal list * Goal.goal list) list
   * Goal.goal list
+  * Goal.goal list
   * Evd.evar_map
 
 (*** General proof functions ***)
@@ -64,9 +66,11 @@ 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 [HasGivenUpGoals] if some goals have been given up.
     Raises [HasUnresolvedEvar] if some evars have been left undefined. *)
 exception UnfinishedProof
 exception HasShelvedGoals
+exception HasGivenUpGoals
 exception HasUnresolvedEvar
 val return : proof -> Evd.evar_map
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 3c0e290236..ac61f4e679 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -262,7 +262,7 @@ let set_used_variables l =
       pstates := { p with section_vars = Some ctx} :: rest
 
 let get_open_goals () =
-  let gl, gll, shelf , _ = 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) +
@@ -297,6 +297,9 @@ let return_proof () =
    | Proof.HasShelvedGoals ->
        raise (Errors.UserError("last tactic before Qed",
          str"Attempt to save a proof with shelved goals"))
+   | Proof.HasGivenUpGoals ->
+       raise (Errors.UserError("last tactic before Qed",
+         str"Attempt to save a proof with given up 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 f086895386..dd05184c40 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -565,7 +565,7 @@ 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 =
@@ -574,7 +574,7 @@ let shelve =
   let (>>) = Proof.seq in
   Proof.get >>= fun initial ->
   Proof.set {initial with comb=[]} >>
-  Proof.put (true,initial.comb)
+  Proof.put (true,(initial.comb,[]))
 
 (* Shelves the unifiable goals under focus, i.e. the goals which
    appear in other goals under focus (the unfocused goals are not
@@ -586,13 +586,23 @@ let shelve_unifiable =
   Proof.get >>= fun initial ->
   let (u,n) = Goal.partition_unifiable initial.solution initial.comb in
   Proof.set {initial with comb=n} >>
-  Proof.put (true,u)
+  Proof.put (true,(u,[]))
 
 (* [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 }
 
+(* Gives up on the goal under focus. Reports an unsafe status. Proofs
+   with given up goals cannot be closed. *)
+let give_up =
+  (* 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 (false,([],initial.comb))
+
 (*** Commands ***)
 
 let in_proofview p k =
@@ -716,7 +726,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 0899f52ddb..635f2fd47a 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -120,7 +120,9 @@ 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*Goal.goal list)
+val apply : Environ.env -> 'a tactic -> proofview -> 'a
+                                                   * proofview
+                                                   * (bool*(Goal.goal list*Goal.goal list))
 
 (*** tacticals ***)
 
@@ -223,6 +225,11 @@ val shelve_unifiable : unit tactic
    goals of p *)
 val unshelve : Goal.goal list -> proofview -> proofview
 
+
+(* Gives up on the goal under focus. Reports an unsafe status. Proofs
+   with given up goals cannot be closed. *)
+val give_up : unit tactic
+
 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 b813eabaab..18f834910b 100644
--- a/proofs/proofview_gen.ml
+++ b/proofs/proofview_gen.ml
@@ -101,7 +101,8 @@ type proofview = { initial : (Term.constr*Term.types)
 
 type logicalState = proofview
 
-type logicalMessageType = bool*Goal.goal list
+type logicalMessageType =
+  bool*(Goal.goal list*Goal.goal list)
 
 type logicalEnvironment = Environ.env
 
@@ -187,68 +188,73 @@ module Logical =
  struct 
   type 'a t =
     __ -> ('a -> 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
+    -> (__ -> (bool*(Goal.goal list*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 -> __ -> (__
-    -> __ -> (__ -> (bool*Goal.goal list) ->
+    -> __ -> (__ -> (exn -> __ IOBase.coq_T)
+    -> __ IOBase.coq_T) -> (exn -> __
+    IOBase.coq_T) -> __ IOBase.coq_T) ->
+    Environ.env -> __ -> (__ ->
+    (bool*(Goal.goal list*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) -> proofview -> __ ->
+    (__ -> __ -> (__ -> (bool*(Goal.goal
+    list*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
+    IOBase.coq_T) -> Environ.env -> __ -> (__
+    -> (bool*(Goal.goal list*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
   
   (** val ret :
       'a1 -> __ -> ('a1 -> proofview -> __ ->
-      ('a2 -> __ -> (__ -> (bool*Goal.goal
-      list) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) ->
+      ('a2 -> __ -> (__ -> (bool*(Goal.goal
+      list*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*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*Goal.goal list) -> __ -> (__
-      -> (exn -> __ IOBase.coq_T) -> __
+      Environ.env -> __ -> (__ ->
+      (bool*(Goal.goal list*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*(Goal.goal
+      list*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 ->
+      (bool*(Goal.goal list*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) -> __
-      -> ('a4 -> (exn -> 'a5 IOBase.coq_T) ->
-      'a5 IOBase.coq_T) -> (exn -> 'a5
-      IOBase.coq_T) -> 'a5 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)
@@ -256,37 +262,39 @@ module Logical =
   (** val bind :
       'a1 t -> ('a1 -> 'a2 t) -> __ -> ('a2
       -> proofview -> __ -> ('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 -> __
+      -> (bool*(Goal.goal list*Goal.goal
+      list)) -> __ -> (__ -> (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) -> __ -> (__ -> (exn ->
+      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+      (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> Environ.env -> __ ->
+      (__ -> (bool*(Goal.goal list*Goal.goal
+      list)) -> __ -> (__ -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
-      proofview -> __ -> ('a3 -> __ -> ('a4
-      -> (bool*Goal.goal list) -> __ -> (__
-      -> (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) -> proofview -> __ ->
+      ('a3 -> __ -> ('a4 -> (bool*(Goal.goal
+      list*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*Goal.goal list) -> __ -> ('a5 ->
+      (bool*(Goal.goal list*Goal.goal list))
+      -> __ -> ('a5 -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) ->
       (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
-      IOBase.coq_T) -> 'a6 IOBase.coq_T **)
+      IOBase.coq_T) -> __ -> ('a5 -> (exn ->
+      'a6 IOBase.coq_T) -> 'a6 IOBase.coq_T)
+      -> (exn -> 'a6 IOBase.coq_T) -> 'a6
+      IOBase.coq_T **)
   
   let bind x k =
     (); (fun _ k0 s ->
@@ -295,37 +303,40 @@ module Logical =
   
   (** val ignore :
       'a1 t -> __ -> (unit -> proofview -> __
-      -> ('a2 -> __ -> (__ -> (bool*Goal.goal
-      list) -> __ -> (__ -> (exn -> __
+      -> ('a2 -> __ -> (__ ->
+      (bool*(Goal.goal list*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 -> __
+      (__ -> (bool*(Goal.goal list*Goal.goal
+      list)) -> __ -> (__ -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
-      proofview -> __ -> ('a2 -> __ -> ('a3
-      -> (bool*Goal.goal list) -> __ -> (__
-      -> (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) -> proofview -> __ ->
+      ('a2 -> __ -> ('a3 -> (bool*(Goal.goal
+      list*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 ->
+      (bool*(Goal.goal list*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) -> __
-      -> ('a4 -> (exn -> 'a5 IOBase.coq_T) ->
-      'a5 IOBase.coq_T) -> (exn -> 'a5
-      IOBase.coq_T) -> 'a5 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 ->
@@ -334,37 +345,39 @@ module Logical =
   (** val seq :
       unit t -> 'a1 t -> __ -> ('a1 ->
       proofview -> __ -> ('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 -> __
+      (bool*(Goal.goal list*Goal.goal list))
+      -> __ -> (__ -> (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) -> __ -> (__ -> (exn ->
+      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+      (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> Environ.env -> __ ->
+      (__ -> (bool*(Goal.goal list*Goal.goal
+      list)) -> __ -> (__ -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
-      proofview -> __ -> ('a2 -> __ -> ('a3
-      -> (bool*Goal.goal list) -> __ -> (__
-      -> (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) -> proofview -> __ ->
+      ('a2 -> __ -> ('a3 -> (bool*(Goal.goal
+      list*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 ->
+      (bool*(Goal.goal list*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) -> __
-      -> ('a4 -> (exn -> 'a5 IOBase.coq_T) ->
-      'a5 IOBase.coq_T) -> (exn -> 'a5
-      IOBase.coq_T) -> 'a5 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 seq x k =
     (); (fun _ k0 s ->
@@ -374,74 +387,79 @@ module Logical =
   (** val set :
       logicalState -> __ -> (unit ->
       proofview -> __ -> ('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 -> __
+      (bool*(Goal.goal list*Goal.goal list))
+      -> __ -> (__ -> (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) -> __ -> (__ -> (exn ->
+      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+      (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> Environ.env -> __ ->
+      (__ -> (bool*(Goal.goal list*Goal.goal
+      list)) -> __ -> (__ -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
-      proofview -> __ -> ('a1 -> __ -> ('a2
-      -> (bool*Goal.goal list) -> __ -> (__
-      -> (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) -> proofview -> __ ->
+      ('a1 -> __ -> ('a2 -> (bool*(Goal.goal
+      list*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 ->
+      (bool*(Goal.goal list*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) -> __
-      -> ('a3 -> (exn -> 'a4 IOBase.coq_T) ->
-      'a4 IOBase.coq_T) -> (exn -> 'a4
-      IOBase.coq_T) -> 'a4 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 set s =
     (); (fun _ k x -> Obj.magic k () s)
   
   (** val get :
       __ -> (logicalState -> proofview -> __
-      -> ('a1 -> __ -> (__ -> (bool*Goal.goal
-      list) -> __ -> (__ -> (exn -> __
+      -> ('a1 -> __ -> (__ ->
+      (bool*(Goal.goal list*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 -> __
+      (__ -> (bool*(Goal.goal list*Goal.goal
+      list)) -> __ -> (__ -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
-      proofview -> __ -> ('a1 -> __ -> ('a2
-      -> (bool*Goal.goal list) -> __ -> (__
-      -> (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) -> proofview -> __ ->
+      ('a1 -> __ -> ('a2 -> (bool*(Goal.goal
+      list*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 ->
+      (bool*(Goal.goal list*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) -> __
-      -> ('a3 -> (exn -> 'a4 IOBase.coq_T) ->
-      'a4 IOBase.coq_T) -> (exn -> 'a4
-      IOBase.coq_T) -> 'a4 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
@@ -449,117 +467,127 @@ module Logical =
   (** val put :
       logicalMessageType -> __ -> (unit ->
       proofview -> __ -> ('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 -> __
+      (bool*(Goal.goal list*Goal.goal list))
+      -> __ -> (__ -> (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) -> __ -> (__ -> (exn ->
+      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+      (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> Environ.env -> __ ->
+      (__ -> (bool*(Goal.goal list*Goal.goal
+      list)) -> __ -> (__ -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
-      proofview -> __ -> ('a1 -> __ -> ('a2
-      -> (bool*Goal.goal list) -> __ -> (__
-      -> (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) -> proofview -> __ ->
+      ('a1 -> __ -> ('a2 -> (bool*(Goal.goal
+      list*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 ->
+      (bool*(Goal.goal list*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) -> __
-      -> ('a3 -> (exn -> 'a4 IOBase.coq_T) ->
-      'a4 IOBase.coq_T) -> (exn -> 'a4
-      IOBase.coq_T) -> 'a4 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 put m =
     (); (fun _ k s _ k0 e _ k1 ->
       Obj.magic k () s __ k0 e __
         (fun b c' ->
         k1 b
-          ((if fst m then fst c' else false),
-          (List.append (snd m) (snd c')))))
+          ((if fst m then fst c' else false),(
+          (List.append (fst (snd m))
+            (fst (snd c'))),(List.append
+                              (snd (snd m))
+                              (snd (snd c')))))))
   
   (** val current :
       __ -> (logicalEnvironment -> proofview
       -> __ -> ('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 -> __
+      (bool*(Goal.goal list*Goal.goal list))
+      -> __ -> (__ -> (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) -> __ -> (__ -> (exn ->
+      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+      (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> Environ.env -> __ ->
+      (__ -> (bool*(Goal.goal list*Goal.goal
+      list)) -> __ -> (__ -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
-      proofview -> __ -> ('a1 -> __ -> ('a2
-      -> (bool*Goal.goal list) -> __ -> (__
-      -> (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) -> proofview -> __ ->
+      ('a1 -> __ -> ('a2 -> (bool*(Goal.goal
+      list*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 ->
+      (bool*(Goal.goal list*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) -> __
-      -> ('a3 -> (exn -> 'a4 IOBase.coq_T) ->
-      'a4 IOBase.coq_T) -> (exn -> 'a4
-      IOBase.coq_T) -> 'a4 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*Goal.goal
-      list) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) ->
+      ('a2 -> __ -> (__ -> (bool*(Goal.goal
+      list*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*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*Goal.goal list) -> __ -> (__
-      -> (exn -> __ IOBase.coq_T) -> __
+      Environ.env -> __ -> (__ ->
+      (bool*(Goal.goal list*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*(Goal.goal
+      list*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 ->
+      (bool*(Goal.goal list*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) -> __
-      -> ('a4 -> (exn -> 'a5 IOBase.coq_T) ->
-      'a5 IOBase.coq_T) -> (exn -> 'a5
-      IOBase.coq_T) -> 'a5 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 ->
@@ -568,37 +596,39 @@ module Logical =
   (** val plus :
       'a1 t -> (exn -> 'a1 t) -> __ -> ('a1
       -> proofview -> __ -> ('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 -> __
+      -> (bool*(Goal.goal list*Goal.goal
+      list)) -> __ -> (__ -> (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) -> __ -> (__ -> (exn ->
+      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+      (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> Environ.env -> __ ->
+      (__ -> (bool*(Goal.goal list*Goal.goal
+      list)) -> __ -> (__ -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
-      proofview -> __ -> ('a2 -> __ -> ('a3
-      -> (bool*Goal.goal list) -> __ -> (__
-      -> (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) -> proofview -> __ ->
+      ('a2 -> __ -> ('a3 -> (bool*(Goal.goal
+      list*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 ->
+      (bool*(Goal.goal list*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) -> __
-      -> ('a4 -> (exn -> 'a5 IOBase.coq_T) ->
-      'a5 IOBase.coq_T) -> (exn -> 'a5
-      IOBase.coq_T) -> 'a5 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 plus x y =
     (); (fun _ k s _ k0 e _ k1 _ sk fk ->
@@ -610,44 +640,47 @@ module Logical =
   (** val split :
       'a1 t -> __ -> (('a1, exn -> 'a1 t)
       list_view -> proofview -> __ -> ('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) -> __ -> (__ ->
+      __ -> (__ -> (bool*(Goal.goal
+      list*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*Goal.goal list) -> __ -> (__
-      -> (exn -> __ IOBase.coq_T) -> __
+      Environ.env -> __ -> (__ ->
+      (bool*(Goal.goal list*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*(Goal.goal
+      list*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 ->
+      (bool*(Goal.goal list*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) -> __
-      -> ('a4 -> (exn -> 'a5 IOBase.coq_T) ->
-      'a5 IOBase.coq_T) -> (exn -> 'a5
-      IOBase.coq_T) -> 'a5 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 split x =
     (); (fun _ k s _ k0 e _ k1 _ sk fk ->
       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,
@@ -662,16 +695,17 @@ module Logical =
         (fun x0 ->
         match x0 with
         | Nil exc ->
-          let c = true,[] in
+          let c = true,([],[]) in
           Obj.magic k (Nil exc) s __ k0 e __
             (fun b c' ->
             k1 b
               ((if fst c
                 then fst c'
-                else false),(List.append
-                              (snd c)
-                              (snd c')))) __
-            sk fk
+                else false),((List.append
+                               (fst (snd c))
+                               (fst (snd c'))),
+              (List.append (snd (snd c))
+                (snd (snd c')))))) __ sk fk
         | Cons (p, y) ->
           let p0,m' = p in
           let a',s' = p0 in
@@ -685,53 +719,60 @@ module Logical =
                 k4 b
                   ((if fst c
                     then fst c'
-                    else false),(List.append
-                                  (snd c)
-                                  (snd c'))))
-                __ sk0 fk1) fk0))) s' __ k0 e
-            __ (fun b c' ->
+                    else false),((List.append
+                                   (fst
+                                    (snd c))
+                                   (fst
+                                    (snd c'))),
+                  (List.append (snd (snd c))
+                    (snd (snd c')))))) __ sk0
+                fk1) fk0))) s' __ k0 e __
+            (fun b c' ->
             k1 b
               ((if fst m'
                 then fst c'
-                else false),(List.append
-                              (snd m')
-                              (snd c')))) __
-            sk fk))
+                else false),((List.append
+                               (fst (snd m'))
+                               (fst (snd c'))),
+              (List.append (snd (snd m'))
+                (snd (snd c')))))) __ sk fk))
   
   (** val lift :
       'a1 NonLogical.t -> __ -> ('a1 ->
       proofview -> __ -> ('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 -> __
+      (bool*(Goal.goal list*Goal.goal list))
+      -> __ -> (__ -> (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) -> __ -> (__ -> (exn ->
+      __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+      (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> Environ.env -> __ ->
+      (__ -> (bool*(Goal.goal list*Goal.goal
+      list)) -> __ -> (__ -> (exn -> __
       IOBase.coq_T) -> __ IOBase.coq_T) ->
-      proofview -> __ -> ('a2 -> __ -> ('a3
-      -> (bool*Goal.goal list) -> __ -> (__
-      -> (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) -> proofview -> __ ->
+      ('a2 -> __ -> ('a3 -> (bool*(Goal.goal
+      list*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 ->
+      (bool*(Goal.goal list*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) -> __
-      -> ('a4 -> (exn -> 'a5 IOBase.coq_T) ->
-      'a5 IOBase.coq_T) -> (exn -> 'a5
-      IOBase.coq_T) -> 'a5 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 lift x =
     (); (fun _ k s _ k0 e _ k1 _ sk fk ->
@@ -739,12 +780,16 @@ module Logical =
         Obj.magic k x0 s __ k0 e __
           (fun b c' ->
           k1 b
-            ((if fst (true,[])
+            ((if fst (true,([],[]))
               then fst c'
-              else false),(List.append
-                            (snd (true,[]))
-                            (snd c')))) __ sk
-          fk))
+              else false),((List.append
+                             (fst
+                               (snd
+                                 (true,([],[]))))
+                             (fst (snd c'))),
+            (List.append
+              (snd (snd (true,([],[]))))
+              (snd (snd c')))))) __ sk fk))
   
   (** val run :
       'a1 t -> logicalEnvironment ->
@@ -755,9 +800,9 @@ 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 (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 c1f1b5ee11..fa4392368c 100644
--- a/proofs/proofview_monad.mli
+++ b/proofs/proofview_monad.mli
@@ -12,8 +12,8 @@ type logicalState = proofview
 
 type logicalEnvironment = Environ.env
 
-(** status (safe/unsafe) * shelved goals *)
-type logicalMessageType = bool * Goal.goal list
+(** status (safe/unsafe) * ( shelved goals * given up ) *)
+type logicalMessageType = bool * ( Goal.goal list * Goal.goal list )