diff options
author | vblot <24938579+vblot@users.noreply.github.com> | 2021-05-28 18:29:37 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-28 18:29:37 +0200 |
commit | e12110637730d067c216abcc86185b761189b342 (patch) | |
tree | c9ed415bbdadb2801e4917aae4a803035b13d4e8 /src/trace/smtMisc.ml | |
parent | 52980aab9541a12619eb9191a94e9b2ba4684447 (diff) | |
download | smtcoq-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.ml | 10 |
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 *) |