diff options
Diffstat (limited to 'toplevel/command.mli')
| -rw-r--r-- | toplevel/command.mli | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/toplevel/command.mli b/toplevel/command.mli index 8a987ef6c..b37c6c359 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -108,10 +108,11 @@ val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr val set_start_hook : (types -> unit) -> unit val start_proof : identifier -> goal_kind -> types -> - declaration_hook -> unit + ?init_tac:Proof_type.tactic -> declaration_hook -> unit -val start_proof_com : identifier option -> goal_kind -> - (local_binder list * constr_expr) -> declaration_hook -> unit +val start_proof_com : goal_kind -> + (lident option * (local_binder list * constr_expr)) list -> + declaration_hook -> unit (* A hook the next three functions pass to cook_proof *) val set_save_hook : (Refiner.pftreestate -> unit) -> unit |