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

16 files changed, 486 insertions, 283 deletions

diff --git a/bootstrap/Monads.v b/bootstrap/Monads.v
index ddfdaecbf..581fafad8 100644
--- a/bootstrap/Monads.v
+++ b/bootstrap/Monads.v
@@ -21,11 +21,20 @@ Extract Inductive list => list [
   "[]"
   "(::)"
 ].
+Opaque app.
+Extraction Implicit app [A].
+Extract Inlined Constant app => "List.append".
 
 (*** Prod ***)
 Extract Inductive prod => "(*)" [
   "(,)"
 ].
+Opaque fst.
+Extraction Implicit fst [A B].
+Extract Inlined Constant fst => "fst".
+Extraction Implicit snd [A B].
+Opaque snd.
+Extract Inlined Constant snd => "snd".
 
 
 (*** Closure elimination **)
@@ -87,6 +96,22 @@ Record T (M:Set) := {
   prod : M -> M -> M
 }.
 
+(** Cartesian product of monoids *)
+Definition cart {M₁} (Mon₁:T M₁) {M₂} (Mon₂:T M₂) : T (M₁*M₂) := {|
+  zero := (Mon₁.(zero _),Mon₂.(zero _));
+  prod x y := (Mon₁.(prod _) (fst x) (fst y), Mon₂.(prod _) (snd x) (snd y))
+|}.
+
+Definition BoolAnd : T bool := {|
+  zero := true;
+  prod := andb
+|}.
+
+Definition List {A:Set} : T (list A) := {|
+  zero := nil ;
+  prod := @app _
+|}.
+
 End Monoid.
 
 (*** Monads and related interfaces ***)
@@ -544,12 +569,10 @@ Record proofview := {
 }.
 
 Definition LogicalState := proofview.
-Definition LogicalMessageType := bool.
+(** Logical Message: status (safe/unsafe) * shelved goals *)
+Definition LogicalMessageType := (bool * list goal)%type.
 Definition LogicalEnvironment := env.
-Definition LogicalMessage : Monoid.T LogicalMessageType := {|
-  Monoid.zero := true;
-  Monoid.prod x y := andb x y
-|}.
+Definition LogicalMessage : Monoid.T LogicalMessageType := Monoid.cart Monoid.BoolAnd Monoid.List.
 
 Definition NonLogicalType := IO.T.
 Definition NonLogicalMonad : Monad NonLogicalType := IO.M.
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 2c77af218..81e7db6dc 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -4614,6 +4614,18 @@ intros; fourier.
 Reset Initial.
 \end{coq_eval}
 
+\section{Non-logical tactics}
+\subsection[\tt shelve]{\tt shelve\tacindex{shelve}\label{shelve}}
+
+This tactic moves all goals under focus to a shelf. While on the shelf, goals
+will not be focused on. They can be solved by unification, or they can be called
+back into focus with the command {\tt Unshelve} (Section~\ref{unshelve}).
+
+\subsection[\tt Unshelve]{\tt Unshelve\comindex{Unshelve}\label{unshelve}}
+
+This command moves all the goals on the shelf (see Section~\ref{shelve}) from the
+shelf into focus, by appending them to the end of the current list of focused goals.
+
 
 \section{Simple tactic macros}
 \index{Tactic macros}
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index 90af0af39..1a333ff16 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -129,13 +129,13 @@ let display mode (view : #GText.view_skel) goals hints evars =
   match goals with
   | None -> ()
     (* No proof in progress *)
-  | Some { Interface.fg_goals = []; Interface.bg_goals = bg } ->
+  | Some { Interface.fg_goals = []; Interface.bg_goals = bg; shelved_goals = shelf } ->
     let bg = flatten (List.rev bg) in
     let evars = match evars with None -> [] | Some evs -> evs in
-    begin match (bg, evars) with
-    | [], [] ->
+    begin match (bg, shelf, evars) with
+    | [], [], [] ->
       view#buffer#insert "No more subgoals."
-    | [], _ :: _ ->
+    | [], [], _ :: _ ->
       (* A proof has been finished, but not concluded *)
       view#buffer#insert "No more subgoals but non-instantiated existential variables:\n\n";
       let iter evar =
@@ -143,7 +143,15 @@ let display mode (view : #GText.view_skel) goals hints evars =
         view#buffer#insert msg
       in
       List.iter iter evars
-    | _, _ ->
+    | [], _, _ ->
+      (* All the goals have been resolved but those on the shelf. *)
+      view#buffer#insert "All the remaining goals are on the shelf:\n\n";
+      let iter goal =
+        let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
+        view#buffer#insert msg
+      in
+      List.iter iter shelf
+    | _, _, _ ->
       (* No foreground proofs, but still unfocused ones *)
       view#buffer#insert "This subproof is complete, but there are still unfocused goals:\n\n";
       let iter goal =
diff --git a/lib/interface.mli b/lib/interface.mli
index a8e3d72bd..d19027256 100644
--- a/lib/interface.mli
+++ b/lib/interface.mli
@@ -44,6 +44,8 @@ type goals = {
   (** List of the focussed goals *)
   bg_goals : (goal list * goal list) list;
   (** Zipper representing the unfocussed background goals *)
+  shelved_goals : goal list;
+  (** List of the goals on the shelf. *)
 }
 
 type hint = (string * string) list
diff --git a/lib/serialize.ml b/lib/serialize.ml
index 88bf87c13..f3c06d930 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -258,13 +258,15 @@ let of_goals g =
   let of_glist = of_list of_goal in
   let fg = of_list of_goal g.fg_goals in
   let bg = of_list (of_pair of_glist of_glist) g.bg_goals in
-  Element ("goals", [], [fg; bg])
+  let shelf = of_list of_goal g.shelved_goals in
+  Element ("goals", [], [fg; bg; shelf])
 let to_goals = function
-  | Element ("goals", [], [fg; bg]) ->
+  | Element ("goals", [], [fg; bg; shelf]) ->
     let to_glist = to_list to_goal in
     let fg = to_list to_goal fg in
     let bg = to_list (to_pair to_glist to_glist) bg in
-    { fg_goals = fg; bg_goals = bg; }
+    let shelf = to_list to_goal shelf in
+    { fg_goals = fg; bg_goals = bg; shelved_goals = shelf; }
   | _ -> raise Marshal_error
 
 let of_coq_info info =
diff --git a/printing/printer.ml b/printing/printer.ml
index 47b52b72b..d91829420 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -423,14 +423,40 @@ let emacs_print_dependent_evars sigma seeds =
    and printed in its entirety. *)
 (* courtieu: in emacs mode, even less cases where the first goal is printed
    in its entirety *)
-let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds stack goals =
+let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals =
+  (** Printing functions for the extra informations. *)
   let rec print_stack a = function
     | [] -> Pp.int a
     | b::l -> Pp.int a ++ str"-" ++ print_stack b l
   in
-  let print_unfocused a l =
-    str"unfocused: " ++ print_stack a l
+  let print_unfocused l =
+    match l with
+    | [] -> None
+    | a::l -> Some (str"unfocused: " ++ print_stack a l)
+  in
+  let print_shelf l =
+    match l with
+    | [] -> None
+    | _ -> Some (str"shelved: " ++ Pp.int (List.length l))
+  in
+  let rec print_comma_separated_list a l =
+    match l with
+    | [] -> a
+    | b::l -> print_comma_separated_list (a++str", "++b) l
+  in
+  let print_extra_list l =
+    match l with
+    | [] -> Pp.mt ()
+    | a::l -> Pp.spc () ++ str"(" ++ print_comma_separated_list a l ++ str")"
   in
+  let extra = Option.List.flatten [ print_unfocused stack ; print_shelf shelf ] in
+  let print_extra = print_extra_list extra in
+  let focused_if_needed =
+    let needed = not (CList.is_empty extra) && pr_first in
+    if needed then str" focused "
+    else str" " (* non-breakable space *)
+  in
+  (** Main function *)
   let rec pr_rec n = function
     | [] -> (mt ())
     | g::rest ->
@@ -445,8 +471,8 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds stack goals =
     else 
       pr_rec 1 (g::l)
   in
-  match goals,stack with
-  | [],_ ->
+  match goals with
+  | [] ->
       begin
 	match close_cmd with
 	  Some cmd ->
@@ -464,31 +490,18 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds stack goals =
 	       ++ emacs_print_dependent_evars sigma seeds ++ fnl () ++
                  str "You can use Grab Existential Variables.")
       end
-  | [g],[] when not !Flags.print_emacs ->
-      let pg = default_pr_goal { it = g ; sigma = sigma; } in
-      v 0 (
-	str "1 subgoal" ++ pr_goal_tag g ++ cut () ++ pg
-	++ emacs_print_dependent_evars sigma seeds
-      )
-  | [g],a::l when not !Flags.print_emacs ->
+  | [g] when not !Flags.print_emacs ->
       let pg = default_pr_goal { it = g ; sigma = sigma; } in
       v 0 (
-	str "1 focused subgoal (" ++ print_unfocused a l ++ str")" ++ pr_goal_tag g ++ cut () ++ pg
+	str "1" ++ focused_if_needed ++ str"subgoal" ++ print_extra
+        ++ pr_goal_tag g ++ cut () ++ pg
 	++ emacs_print_dependent_evars sigma seeds
       )
-  | g1::rest,[] ->
+  | g1::rest ->
       let goals = print_multiple_goals g1 rest in
       v 0 (
-	int(List.length rest+1) ++ str" subgoals" ++
-          str (emacs_str ", subgoal 1") ++ pr_goal_tag g1 ++ cut ()
-	++ goals
-	++ emacs_print_dependent_evars sigma seeds
-      )
-  | g1::rest,a::l ->
-      let goals = print_multiple_goals g1 rest in
-      v 0 (
-	int(List.length rest+1) ++ str" focused subgoals (" ++
-          print_unfocused a l ++ str")" ++ cut () ++
+	int(List.length rest+1) ++ focused_if_needed ++ str"subgoals" ++
+          print_extra ++ cut () ++
           str (emacs_str ", subgoal 1") ++ pr_goal_tag g1 ++ cut ()
 	++ goals
 	++ emacs_print_dependent_evars sigma seeds
@@ -499,7 +512,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds stack goals =
 
 
 type printer_pr = {
- pr_subgoals            : ?pr_first:bool -> string option -> evar_map -> evar list -> int list -> goal list -> std_ppcmds;
+ pr_subgoals            : ?pr_first:bool -> string option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds;
  pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds;
  pr_goal                : goal sigma -> std_ppcmds;
 }
@@ -527,21 +540,29 @@ let pr_open_subgoals () =
      straightforward, but seriously, [Proof.proof] should return
      [evar_info]-s instead. *)
   let p = Proof_global.give_me_the_proof () in
-  let (goals , stack , sigma ) = Proof.proof p in
+  let (goals , stack , shelf, sigma ) = Proof.proof p in
   let stack = List.map (fun (l,r) -> List.length l + List.length r) stack in
   let seeds = Proof.V82.top_evars p in
   begin match goals with
   | [] -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in
-          begin match bgoals with
-	  | [] -> pr_subgoals None sigma seeds stack goals
-	  | _ ->
+          begin match bgoals,shelf with
+	  | [],[] -> pr_subgoals None sigma seeds shelf stack goals
+          | [] , _ ->
+	    (* emacs mode: xml-like flag for detecting information message *)
+	    str (emacs_str "<infomsg>") ++
+	    str "All the remaining goals are on the shelf."
+	    ++ str (emacs_str "</infomsg>")
+	    ++ fnl () ++ fnl ()
+            ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] shelf
+	  | _ , _ ->
 	    (* emacs mode: xml-like flag for detecting information message *)
 	    str (emacs_str "<infomsg>") ++
 	    str "This subproof is complete, but there are still unfocused goals."
 	    ++ str (emacs_str "</infomsg>")
-	    ++ fnl () ++ fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds [] bgoals
+	    ++ fnl () ++ fnl ()
+            ++ pr_subgoals ~pr_first:false None bsigma seeds shelf [] bgoals
 	  end
-  | _ -> pr_subgoals None sigma seeds stack goals
+  | _ -> pr_subgoals None sigma seeds shelf stack goals
   end
 
 let pr_nth_open_subgoal n =
diff --git a/printing/printer.mli b/printing/printer.mli
index 8a698203a..2d7f0a5d3 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -122,7 +122,7 @@ val pr_transparent_state   : transparent_state -> std_ppcmds
 (** Proofs *)
 
 val pr_goal                : goal sigma -> std_ppcmds
-val pr_subgoals            : ?pr_first:bool -> string option -> evar_map -> evar list -> int list -> goal list -> std_ppcmds
+val pr_subgoals            : ?pr_first:bool -> string option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds
 val pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds
 val pr_concl               : int -> evar_map -> goal -> std_ppcmds
 
@@ -159,7 +159,7 @@ val pr_assumptionset :
 val pr_goal_by_id : string -> std_ppcmds
 
 type printer_pr = {
- pr_subgoals            : ?pr_first:bool -> string option -> evar_map -> evar list -> int list -> goal list -> std_ppcmds;
+ pr_subgoals            : ?pr_first:bool -> string option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds;
  pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds;
  pr_goal                : goal sigma -> std_ppcmds;
 };;
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
 
 
 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 436e3bd5b..44719a962 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -803,3 +803,16 @@ VERNAC COMMAND EXTEND GrabEvars
   => [ Vernacexpr.VtProofStep, Vernacexpr.VtLater ]
   -> [ Proof_global.simple_with_current_proof (fun _ p  -> Proof.V82.grab_evars p) ]
 END
+
+(* Shelves all the goals under focus. *)
+TACTIC EXTEND shelve
+| [ "shelve" ] ->
+    [ Proofview.shelve ]
+END
+
+(* Command to add every unshelved variables to the focus *)
+VERNAC COMMAND EXTEND Unshelve
+[ "Unshelve" ]
+  => [ Vernacexpr.VtProofStep, Vernacexpr.VtLater ]
+  -> [ Proof_global.simple_with_current_proof (fun _ p  -> Proof.unshelve p) ]
+END
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index fc0f4f22a..48afe324e 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -193,7 +193,7 @@ let goals () =
   if not (String.is_empty s) then msg_info (str s);
   try
     let pfts = Proof_global.give_me_the_proof () in
-    let (goals, zipper, sigma) = Proof.proof pfts in
+    let (goals, zipper, shelf, sigma) = Proof.proof pfts in
     let fg = List.map (process_goal sigma) goals in
     let map_zip (lg, rg) =
       let lg = List.map (process_goal sigma) lg in
@@ -201,7 +201,8 @@ let goals () =
       (lg, rg)
     in
     let bg = List.map map_zip zipper in
-    Some { Interface.fg_goals = fg; Interface.bg_goals = bg; }
+    let shelf = List.map (process_goal sigma) shelf in
+    Some { Interface.fg_goals = fg; Interface.bg_goals = bg; shelved_goals = shelf; }
   with Proof_global.NoCurrentProof -> None
 
 let evars () =