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.mli16
1 files changed, 8 insertions, 8 deletions
diff --git a/src/verit/verit.mli b/src/verit/verit.mli
index 4583bbd..72566d2 100644
--- a/src/verit/verit.mli
+++ b/src/verit/verit.mli
@@ -11,13 +11,13 @@
val parse_certif :
- Structures.id ->
- Structures.id ->
- Structures.id ->
- Structures.id ->
- Structures.id -> Structures.id -> Structures.id -> string -> string -> unit
+ CoqInterface.id ->
+ CoqInterface.id ->
+ CoqInterface.id ->
+ CoqInterface.id ->
+ CoqInterface.id -> CoqInterface.id -> CoqInterface.id -> string -> string -> unit
val checker : string -> string -> unit
val checker_debug : string -> string -> unit
-val theorem : Structures.id -> string -> string -> unit
-val tactic : EConstr.t -> Structures.constr_expr list -> Structures.tactic
-val tactic_no_check : EConstr.t -> Structures.constr_expr list -> Structures.tactic
+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