Proof_global: fix start_proof comment after the preceding commits.

2 files changed, 12 insertions, 11 deletions

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 2f002e941c..1ed63511da 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -237,12 +237,12 @@ let _ = Errors.register_handler begin function
   | _ -> raise Errors.Unhandled
 end
 
-(* [start_proof id str goals terminator] starts a proof of name [id]
-   with goals [goals] (a list of pairs of environment and
-   conclusion); at the end of the proof [terminator] is called to
-   close the proof. It raises exception [ProofInProgress] if there
-   is a proof being currently edited. *)
-
+(** [start_proof id str goals terminator] starts a proof of name [id]
+    with goals [goals] (a list of pairs of environment and
+    conclusion); [str] describes what kind of theorem/definition this
+    is (spiwack: for potential printing, I believe is used only by
+    closing commands and the xml plugin); [terminator] is used at the
+    end of the proof to close the proof. *)
 let start_proof id str goals terminator =
   let initial_state = {
     pid = id;
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index ed7668d576..0000fe9744 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -64,11 +64,12 @@ type proof_terminator =
     proof_ending -> unit
 type closed_proof = proof_object*proof_terminator Ephemeron.key
 
-(** [start_proof s str goals ~init_tac ~compute_guard 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). *)
+(** [start_proof id str goals terminator] starts a proof of name [id]
+    with goals [goals] (a list of pairs of environment and
+    conclusion); [str] describes what kind of theorem/definition this
+    is (spiwack: for potential printing, I believe is used only by
+    closing commands and the xml plugin); [terminator] is used at the
+    end of the proof to close the proof. *)
 val start_proof : Names.Id.t ->
                           Decl_kinds.goal_kind ->
                           (Environ.env * Term.types) list  ->