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 6fa62d8..4b84b58 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 : Structures.id -> string -> string -> unit
-val tactic : Structures.constr list -> Structures.constr_expr list -> Structures.tactic
-val tactic_no_check : Structures.constr list -> Structures.constr_expr list -> Structures.tactic
+val tactic : EConstr.t -> Structures.constr_expr list -> Structures.tactic
+val tactic_no_check : EConstr.t -> Structures.constr_expr list -> Structures.tactic