aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/decl_mode/decl_proof_instr.mli
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/decl_mode/decl_proof_instr.mli')
-rw-r--r--plugins/decl_mode/decl_proof_instr.mli4
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