diff options
Diffstat (limited to 'plugins/decl_mode/decl_proof_instr.mli')
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.mli b/plugins/decl_mode/decl_proof_instr.mli index 107b65366..d78ca84d1 100644 --- a/plugins/decl_mode/decl_proof_instr.mli +++ b/plugins/decl_mode/decl_proof_instr.mli @@ -15,9 +15,9 @@ open Decl_mode val go_to_proof_mode: unit -> unit val return_from_tactic_mode: unit -> unit -val register_automation_tac: tactic -> unit +val register_automation_tac: unit Proofview.tactic -> unit -val automation_tac : tactic +val automation_tac : unit Proofview.tactic val concl_refiner: Termops.meta_type_map -> constr -> Proof_type.goal sigma -> constr |