From e12110637730d067c216abcc86185b761189b342 Mon Sep 17 00:00:00 2001
From: vblot <24938579+vblot@users.noreply.github.com>
Date: Fri, 28 May 2021 18:29:37 +0200
Subject: getting rid of native-coq (#95)

---
 src/verit/verit.mli | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'src/verit/verit.mli')

diff --git a/src/verit/verit.mli b/src/verit/verit.mli
index 0560d77..f0acd0c 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
-- 
cgit