diff options
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. |