From aa72a2e5a980bb02258d60965346740d7cf98cee Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 14 Jun 2002 12:27:19 +0000
Subject: Commentaires

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2786 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/pfedit.mli | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index bb828e287c..bb66cb6891 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 *
-- 
cgit v1.2.3