From 4ac1b34ff8afc250e34d0b229c0a3608ed83e640 Mon Sep 17 00:00:00 2001 From: aspiwack Date: Sat, 2 Nov 2013 15:41:49 +0000 Subject: Update comments. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17033 85f007b7-540e-0410-9357-904b9bb8a0f7 --- proofs/proof.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'proofs/proof.ml') diff --git a/proofs/proof.ml b/proofs/proof.ml index 99654ab75..1dca04336 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -7,10 +7,9 @@ (************************************************************************) (* Module defining the last essential tiles of interactive proofs. - The features of the Proof module are undoing and focusing. - A proof is a mutable object, it contains a proofview, and some information - to be able to undo actions, and to unfocus the current view. All three - of these being meant to evolve. + A proof deals with the focusing commands (including the braces and bullets), + the shelf (see the [shelve] tactic) and given up goal (see the [give_up] + tactic). A proof is made of the following: - Proofview: a proof is primarily the data of the current view. That which is shown to the user (as a remainder, a proofview is mainly the logical state of the proof, together with the @@ -23,10 +22,11 @@ the focus kind is actually stored inside the condition). To unfocus, one needs to know the focus kind, and the condition (for instance "no condition" or the proof under focused must be complete) must be met. - - Undo: since proofviews and focus stacks are immutable objects, - it could suffice to hold the previous states, to allow to return to the past. - However, we also allow other modules to do actions that can be undone. - Therefore the undo stack stores action to be ran to undo. + - Shelf: A list of goals which have been put aside during the proof. They can be + retrieved with the [Unshelve] command, or solved by side effects + - Given up goals: as long as there is a given up goal, the proof is not completed. + Given up goals cannot be retrieved, the user must go back where the tactic + [give_up] was run and solve the goal there. *) open Util -- cgit v1.2.3