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/trace/smtAtom.mli | 26 +++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

(limited to 'src/trace/smtAtom.mli')

diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli
index 645a638..27737ff 100644
--- a/src/trace/smtAtom.mli
+++ b/src/trace/smtAtom.mli
@@ -76,14 +76,14 @@ module Op :
 
     val create : unit -> reify_tbl
 
-    val declare : reify_tbl -> Structures.constr -> btype array ->
+    val declare : reify_tbl -> CoqInterface.constr -> btype array ->
                   btype -> string option -> indexed_op
 
-    val of_coq : reify_tbl -> Structures.constr -> indexed_op
+    val of_coq : reify_tbl -> CoqInterface.constr -> indexed_op
 
-    val interp_tbl : Structures.constr ->
-      (btype array -> btype -> Structures.constr -> Structures.constr) ->
-      reify_tbl -> Structures.constr
+    val interp_tbl : CoqInterface.constr ->
+      (btype array -> btype -> CoqInterface.constr -> CoqInterface.constr) ->
+      reify_tbl -> CoqInterface.constr
 
     val to_list : reify_tbl -> (int * (btype array) * btype * indexed_op) list
 
@@ -142,18 +142,18 @@ module Atom :
       (** Given a coq term, build the corresponding atom *)
       exception UnknownUnderForall
       val of_coq : ?eqsym:bool -> SmtBtype.reify_tbl -> Op.reify_tbl ->
-        reify_tbl -> SmtMisc.logic -> Environ.env -> Evd.evar_map -> Structures.constr -> t
+        reify_tbl -> SmtMisc.logic -> Environ.env -> Evd.evar_map -> CoqInterface.constr -> t
 
-      val get_coq_term_op : int -> Structures.constr
+      val get_coq_term_op : int -> CoqInterface.constr
 
-      val to_coq : t -> Structures.constr
+      val to_coq : t -> CoqInterface.constr
 
       val to_array : reify_tbl -> 'a -> (atom -> 'a) -> 'a array
 
-      val interp_tbl : reify_tbl -> Structures.constr
+      val interp_tbl : reify_tbl -> CoqInterface.constr
 
-      val interp_to_coq : Structures.constr -> (int, Structures.constr) Hashtbl.t ->
-	t -> Structures.constr
+      val interp_to_coq : CoqInterface.constr -> (int, CoqInterface.constr) Hashtbl.t ->
+	t -> CoqInterface.constr
 
       val logic : t -> SmtMisc.logic
 
@@ -201,5 +201,5 @@ module Trace : sig
 end
 
 
-val make_t_i : SmtBtype.reify_tbl -> Structures.constr
-val make_t_func : Op.reify_tbl -> Structures.constr -> Structures.constr
+val make_t_i : SmtBtype.reify_tbl -> CoqInterface.constr
+val make_t_func : Op.reify_tbl -> CoqInterface.constr -> CoqInterface.constr
-- 
cgit