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

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

diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml
index d750550..165814b 100644
--- a/src/trace/smtMisc.ml
+++ b/src/trace/smtMisc.ml
@@ -16,7 +16,7 @@ let cInt_tbl = Hashtbl.create 17
 let mkInt i = 
   try Hashtbl.find cInt_tbl i 
   with Not_found ->
-    let ci = Structures.mkInt i in
+    let ci = CoqInterface.mkInt i in
     Hashtbl.add cInt_tbl i ci;
     ci
 
@@ -25,15 +25,15 @@ type 'a gen_hashed = { index : int; hval : 'a }
 
 
 (** Functions over constr *)
-let mklApp f args = Structures.mkApp (Lazy.force f, args)
+let mklApp f args = CoqInterface.mkApp (Lazy.force f, args)
 
-let string_of_name_def d n = try Structures.string_of_name n with | _ -> d
+let string_of_name_def d n = try CoqInterface.string_of_name n with | _ -> d
 
 let string_coq_constr t =
   let rec fix rf x = rf (fix rf) x in
   let pr = fix
-      Ppconstr.modular_constr_pr Pp.mt Structures.ppconstr_lsimpleconstr in
-  Pp.string_of_ppcmds (pr (Structures.constrextern_extern_constr t))
+      Ppconstr.modular_constr_pr Pp.mt CoqInterface.ppconstr_lsimpleconstr in
+  Pp.string_of_ppcmds (pr (CoqInterface.constrextern_extern_constr t))
 
 
 (** Logics *)
-- 
cgit