diff options
| -rw-r--r-- | proofs/proof_global.ml | 12 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 11 |
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 -> |