aboutsummaryrefslogtreecommitdiffstats
path: root/src/trace/smtMisc.ml
diff options
context:
space:
mode:
authorvblot <24938579+vblot@users.noreply.github.com>2021-05-28 18:29:37 +0200
committerGitHub <noreply@github.com>2021-05-28 18:29:37 +0200
commite12110637730d067c216abcc86185b761189b342 (patch)
treec9ed415bbdadb2801e4917aae4a803035b13d4e8 /src/trace/smtMisc.ml
parent52980aab9541a12619eb9191a94e9b2ba4684447 (diff)
downloadsmtcoq-e12110637730d067c216abcc86185b761189b342.tar.gz
smtcoq-e12110637730d067c216abcc86185b761189b342.zip
getting rid of native-coq (#95)
Diffstat (limited to 'src/trace/smtMisc.ml')
-rw-r--r--src/trace/smtMisc.ml10
1 files changed, 5 insertions, 5 deletions
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 *)