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/smtMisc.mli | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

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

diff --git a/src/trace/smtMisc.mli b/src/trace/smtMisc.mli
index a6f5db8..5359c15 100644
--- a/src/trace/smtMisc.mli
+++ b/src/trace/smtMisc.mli
@@ -10,12 +10,12 @@
 (**************************************************************************)
 
 
-val cInt_tbl : (int, Structures.constr) Hashtbl.t
-val mkInt : int -> Structures.constr
+val cInt_tbl : (int, CoqInterface.constr) Hashtbl.t
+val mkInt : int -> CoqInterface.constr
 type 'a gen_hashed = { index : int; hval : 'a; }
-val mklApp : Structures.constr Lazy.t -> Structures.constr array -> Structures.constr
-val string_of_name_def : string -> Structures.name -> string
-val string_coq_constr : Structures.constr -> string
+val mklApp : CoqInterface.constr Lazy.t -> CoqInterface.constr array -> CoqInterface.constr
+val string_of_name_def : string -> CoqInterface.name -> string
+val string_coq_constr : CoqInterface.constr -> string
 type logic_item = LUF | LLia | LBitvectors | LArrays
 module SL : Set.S with type elt = logic_item
 type logic = SL.t
-- 
cgit