diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2021-05-28 19:59:39 +0200 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2021-05-28 19:59:39 +0200 |
commit | 220afeb0eb1b0b63fccd29e254f3179cac834c12 (patch) | |
tree | 7ff6cc51b5e09034658fe053ccff4675a964ed13 /src/trace/smtMisc.ml | |
parent | a827528c0435f2006560b8cb359420bbffe85881 (diff) | |
parent | 4c348a170ea80d20f08ccd5b20e98f56b9267485 (diff) | |
download | smtcoq-220afeb0eb1b0b63fccd29e254f3179cac834c12.tar.gz smtcoq-220afeb0eb1b0b63fccd29e254f3179cac834c12.zip |
Merge branch 'coq-8.12' of github.com:smtcoq/smtcoq into coq-8.13
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 *) |