From fb1c2f25fb0ca5f422c69e14b6b434ad1d8f01a9 Mon Sep 17 00:00:00 2001 From: aspiwack Date: Sat, 2 Nov 2013 15:40:19 +0000 Subject: 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 --- bootstrap/Monads.v | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'bootstrap/Monads.v') 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. -- cgit v1.2.3