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

1 files changed, 28 insertions, 5 deletions

diff --git a/bootstrap/Monads.v b/bootstrap/Monads.v
index ddfdaecbf3..581fafad8e 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.