aboutsummaryrefslogtreecommitdiffstats
path: root/src/verit/verit.mli
diff options
context:
space:
mode:
Diffstat (limited to 'src/verit/verit.mli')
-rw-r--r--src/verit/verit.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/verit/verit.mli b/src/verit/verit.mli
index 72566d2..d67051f 100644
--- a/src/verit/verit.mli
+++ b/src/verit/verit.mli
@@ -19,5 +19,5 @@ val parse_certif :
val checker : string -> string -> unit
val checker_debug : string -> string -> unit
val theorem : CoqInterface.id -> string -> string -> unit
-val tactic : EConstr.t -> CoqInterface.constr_expr list -> CoqInterface.tactic
-val tactic_no_check : EConstr.t -> CoqInterface.constr_expr list -> CoqInterface.tactic
+val tactic : int option -> EConstr.t -> CoqInterface.constr_expr list -> CoqInterface.tactic
+val tactic_no_check : int option -> EConstr.t -> CoqInterface.constr_expr list -> CoqInterface.tactic