diff options
| author |  Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
| commit | cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch) | |
| tree | b7832bd5d412a5a5d69cb36ae2ded62c71124c22 /proofs/pfedit.mli | |
| parent | 113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff) | |
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'proofs/pfedit.mli')
| -rw-r--r-- | proofs/pfedit.mli | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 42c24081..464f6286 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pfedit.mli 10850 2008-04-25 18:07:44Z herbelin $ i*) +(*i $Id: pfedit.mli 11745 2009-01-04 18:43:08Z herbelin $ i*) (*i*) open Util @@ -80,7 +80,7 @@ val get_undo : unit -> int option val start_proof : identifier -> goal_kind -> named_context_val -> constr -> - ?init_tac:tactic -> declaration_hook -> unit + ?init_tac:tactic -> ?compute_guard:bool -> declaration_hook -> unit (* [restart_proof ()] restarts the current focused proof from the beginning or fails if no proof is focused *) @@ -104,10 +104,11 @@ val suspend_proof : unit -> unit (*s [cook_proof opacity] turns the current proof (assumed completed) into a constant with its name, kind and possible hook (see [start_proof]); - it fails if there is no current proof of if it is not completed *) + it fails if there is no current proof of if it is not completed; + it also tells if the guardness condition has to be inferred. *) val cook_proof : (Refiner.pftreestate -> unit) -> - identifier * (Entries.definition_entry * goal_kind * declaration_hook) + identifier * (Entries.definition_entry * bool * goal_kind * declaration_hook) (* To export completed proofs to xml *) val set_xml_cook_proof : (goal_kind * pftreestate -> unit) -> unit |