1 files changed, 55 insertions, 9 deletions
diff --git a/src/trace/smtBtype.mli b/src/trace/smtBtype.mli
index 29e91bf..559e809 100644
--- a/src/trace/smtBtype.mli
+++ b/src/trace/smtBtype.mli
@@ -1,18 +1,64 @@
-type indexed_type
-val dummy_indexed_type : int -> indexed_type
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2019                                          *)
+(*                                                                        *)
+(*     See file "AUTHORS" for the list of authors                         *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+open SmtMisc
+
+
+type indexed_type = Term.constr gen_hashed
+
+val dummy_indexed_type: int -> indexed_type
 val indexed_type_index : indexed_type -> int
 val indexed_type_hval : indexed_type -> Term.constr
-type btype = TZ | Tbool | Tpositive | Tindex of indexed_type
-val indexed_type_of_int : int -> indexed_type
+
+type btype =
+  | TZ
+  | Tbool
+  | Tpositive
+  | TBV of int
+  | TFArray of btype * btype
+  | Tindex of indexed_type
+
+val indexed_type_of_int : int -> Term.constr SmtMisc.gen_hashed
+
 val equal : btype -> btype -> bool
+
 val to_coq : btype -> Term.constr
-val to_string : btype -> string
+
 val to_smt : Format.formatter -> btype -> unit
+
 type reify_tbl
+
 val create : unit -> reify_tbl
-val get_cuts : reify_tbl -> (Structures.names_id_t * Term.types) list
+
 val declare : reify_tbl -> Term.constr -> Term.constr -> btype
-val of_coq : reify_tbl -> Term.types -> btype
+
+val of_coq : reify_tbl -> logic -> Term.constr -> btype
+
+val get_coq_type_op : int -> Term.constr
+
 val interp_tbl : reify_tbl -> Term.constr
-val to_list : reify_tbl -> (int * indexed_type) list
-val interp_to_coq : 'a -> btype -> Term.constr
+
+val to_list : reify_tbl ->  (int * indexed_type) list
+
+val make_t_i : reify_tbl -> Term.constr
+
+val dec_interp : Term.constr -> btype -> Term.constr
+val ord_interp : Term.constr -> btype -> Term.constr
+val comp_interp : Term.constr -> btype -> Term.constr
+val inh_interp : Term.constr -> btype -> Term.constr
+val interp : Term.constr -> btype -> Term.constr
+
+val interp_to_coq : reify_tbl -> btype -> Term.constr
+
+val get_cuts : reify_tbl -> (Structures.names_id_t * Term.types) list
+
+val logic : btype -> logic