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.mli | |
| 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.mli')
| -rw-r--r-- | src/trace/smtMisc.mli | 10 |
1 files changed, 5 insertions, 5 deletions
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 |