diff options
Diffstat (limited to 'proofs/pfedit.mli')
| -rw-r--r-- | proofs/pfedit.mli | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index beeb56959..4ddcc5c8d 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -14,7 +14,7 @@ open Names open Term open Sign open Environ -open Nametab +open Decl_kinds open Proof_type open Tacmach (*i*) @@ -67,7 +67,7 @@ val get_undo : unit -> int option declare the built constructions as a coercion or a setoid morphism) *) val start_proof : - identifier -> bool * Libnames.strength -> named_context -> constr + identifier -> goal_kind -> named_context -> constr -> declaration_hook -> unit (* [restart_proof ()] restarts the current focused proof from the beginning @@ -91,12 +91,11 @@ 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, strength and possible hook (see [start_proof]); + 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 *) val cook_proof : unit -> - identifier * - (Entries.definition_entry * (bool * Libnames.strength) * declaration_hook) + identifier * (Entries.definition_entry * goal_kind * declaration_hook) (* To export completed proofs to xml *) val set_xml_cook_proof : (pftreestate -> unit) -> unit |