diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:40:19 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:40:19 +0000 |
| commit | fb1c2f25fb0ca5f422c69e14b6b434ad1d8f01a9 (patch) | |
| tree | 37629e2fd9a96a6eee0ffbbe8d7daf4dca9e7650 /bootstrap/Monads.v | |
| parent | bd39dfc9d8090f50bff6260495be2782e6d5e342 (diff) | |
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
Diffstat (limited to 'bootstrap/Monads.v')
| -rw-r--r-- | bootstrap/Monads.v | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/bootstrap/Monads.v b/bootstrap/Monads.v index 581fafad8..a6b7bad12 100644 --- a/bootstrap/Monads.v +++ b/bootstrap/Monads.v @@ -569,10 +569,12 @@ Record proofview := { }. Definition LogicalState := proofview. -(** Logical Message: status (safe/unsafe) * shelved goals *) -Definition LogicalMessageType := (bool * list goal)%type. +(** Logical Message: status (safe/unsafe) * ( shelved goals * given up ) *) +Definition LogicalMessageType := ( bool * ( list goal * list goal ))%type. Definition LogicalEnvironment := env. -Definition LogicalMessage : Monoid.T LogicalMessageType := Monoid.cart Monoid.BoolAnd Monoid.List. +Definition LogicalMessage : Monoid.T LogicalMessageType := + Monoid.cart Monoid.BoolAnd (Monoid.cart Monoid.List Monoid.List) +. Definition NonLogicalType := IO.T. Definition NonLogicalMonad : Monad NonLogicalType := IO.M. |