diff options
Diffstat (limited to 'src/trace/smtBtype.mli')
| -rw-r--r-- | src/trace/smtBtype.mli | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/src/trace/smtBtype.mli b/src/trace/smtBtype.mli index 5d45ca4..5710cf3 100644 --- a/src/trace/smtBtype.mli +++ b/src/trace/smtBtype.mli @@ -13,11 +13,11 @@ open SmtMisc -type indexed_type = Structures.constr gen_hashed +type indexed_type val dummy_indexed_type: int -> indexed_type val indexed_type_index : indexed_type -> int -val indexed_type_hval : indexed_type -> Structures.constr +val indexed_type_compdec : indexed_type -> Structures.constr type btype = | TZ @@ -27,9 +27,9 @@ type btype = | TFArray of btype * btype | Tindex of indexed_type -val indexed_type_of_int : int -> Structures.constr SmtMisc.gen_hashed +val indexed_type_of_int : int -> indexed_type -val equal : btype -> btype -> bool +module HashedBtype : Hashtbl.HashedType with type t = btype val to_coq : btype -> Structures.constr @@ -39,9 +39,8 @@ type reify_tbl val create : unit -> reify_tbl -val declare : reify_tbl -> Structures.constr -> Structures.constr -> btype - val of_coq : reify_tbl -> logic -> Structures.constr -> btype +val of_coq_compdec : reify_tbl -> Structures.constr -> Structures.constr -> btype val get_coq_type_op : int -> Structures.constr |