diff options
| author | ckeller <ckeller@users.noreply.github.com> | 2019-03-11 20:25:35 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-03-11 20:25:35 +0100 |
| commit | a88e3b3b6ad01a9b85c828b9a1225732275affee (patch) | |
| tree | acc3768695698a80867b4ce941ab4cb7b4b99d7a /src/trace/smtMisc.mli | |
| parent | 33010bfa6345549d8b9b0c06f44150b60d0c86e5 (diff) | |
| download | smtcoq-a88e3b3b6ad01a9b85c828b9a1225732275affee.tar.gz smtcoq-a88e3b3b6ad01a9b85c828b9a1225732275affee.zip | |
V8.8 (#42)
* Towards 8.8
* Towards 8.8
* Towards 8.8
* Towards 8.8
* Towards 8.8
* Towards 8.8
* Towards 8.8
* Organization structures
* 8.8 ok with standard coq
Diffstat (limited to 'src/trace/smtMisc.mli')
| -rw-r--r-- | src/trace/smtMisc.mli | 13 |
1 files changed, 5 insertions, 8 deletions
diff --git a/src/trace/smtMisc.mli b/src/trace/smtMisc.mli index a9de935..f3bcf60 100644 --- a/src/trace/smtMisc.mli +++ b/src/trace/smtMisc.mli @@ -10,15 +10,12 @@ (**************************************************************************) -val cInt_tbl : (int, Term.constr) Hashtbl.t -val mkInt : int -> Term.constr +val cInt_tbl : (int, Structures.constr) Hashtbl.t +val mkInt : int -> Structures.constr type 'a gen_hashed = { index : int; hval : 'a; } -val mklApp : Term.constr Lazy.t -> Term.constr array -> Term.constr -val declare_new_type : Names.variable -> Term.constr -val declare_new_variable : Names.variable -> Term.types -> Term.constr -val mkName : string -> Names.name -val string_coq_constr : Term.constr -> string -val string_of_name : Names.name -> string +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 type logic_item = LUF | LLia | LBitvectors | LArrays module SL : Set.S with type elt = logic_item type logic = SL.t |