diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-06-14 12:27:19 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-06-14 12:27:19 +0000 |
| commit | aa72a2e5a980bb02258d60965346740d7cf98cee (patch) | |
| tree | c1cd38729059b6706f42e95200c47f602cf9e4fa | |
| parent | 100120634953b594169931409122c580fa12e5b1 (diff) | |
Commentaires
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2786 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | proofs/pfedit.mli | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index bb828e287..bb66cb689 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -62,7 +62,9 @@ val undo : int -> unit val set_undo : int option -> unit val get_undo : unit -> int option -(*s [start_proof s str env t] starts a proof of name [s] and conclusion [t] *) +(*s [start_proof s str env t hook] starts a proof of name [s] and conclusion + [t]; [hook] is optionally a function to be applied at proof end (e.g. to + declare the built constructions as a coercion or a setoid morphism) *) val start_proof : identifier -> bool * strength -> named_context -> constr @@ -88,9 +90,9 @@ val resume_proof : identifier -> unit val suspend_proof : unit -> unit -(*s [cook_proof opacity] turns the current proof (assumed completed) - into a constant with its name and strength; it fails if there is - no current proof of if it is not completed *) +(*s [cook_proof opacity] turns the current proof (assumed completed) into + a constant with its name, strength and possible hook (see [start_proof]); + it fails if there is no current proof of if it is not completed *) val cook_proof : unit -> identifier * |