From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 1 Feb 2009 00:54:40 +0100 Subject: Imported Upstream version 8.2~rc2+dfsg --- proofs/pfedit.mli | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'proofs/pfedit.mli') 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 -- cgit v1.2.3