diff options
Diffstat (limited to 'src/trace/smtBtype.mli')
| -rw-r--r-- | src/trace/smtBtype.mli | 32 |
1 files changed, 16 insertions, 16 deletions
diff --git a/src/trace/smtBtype.mli b/src/trace/smtBtype.mli index 4f8d4ad..5d45ca4 100644 --- a/src/trace/smtBtype.mli +++ b/src/trace/smtBtype.mli @@ -13,11 +13,11 @@ open SmtMisc -type indexed_type = Term.constr gen_hashed +type indexed_type = Structures.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 +val indexed_type_hval : indexed_type -> Structures.constr type btype = | TZ @@ -27,11 +27,11 @@ type btype = | TFArray of btype * btype | Tindex of indexed_type -val indexed_type_of_int : int -> Term.constr SmtMisc.gen_hashed +val indexed_type_of_int : int -> Structures.constr SmtMisc.gen_hashed val equal : btype -> btype -> bool -val to_coq : btype -> Term.constr +val to_coq : btype -> Structures.constr val to_smt : Format.formatter -> btype -> unit @@ -39,26 +39,26 @@ type reify_tbl val create : unit -> reify_tbl -val declare : reify_tbl -> Term.constr -> Term.constr -> btype +val declare : reify_tbl -> Structures.constr -> Structures.constr -> btype -val of_coq : reify_tbl -> logic -> Term.constr -> btype +val of_coq : reify_tbl -> logic -> Structures.constr -> btype -val get_coq_type_op : int -> Term.constr +val get_coq_type_op : int -> Structures.constr -val interp_tbl : reify_tbl -> Term.constr +val interp_tbl : reify_tbl -> Structures.constr val to_list : reify_tbl -> (int * indexed_type) list -val make_t_i : reify_tbl -> Term.constr +val make_t_i : reify_tbl -> Structures.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 dec_interp : Structures.constr -> btype -> Structures.constr +val ord_interp : Structures.constr -> btype -> Structures.constr +val comp_interp : Structures.constr -> btype -> Structures.constr +val inh_interp : Structures.constr -> btype -> Structures.constr +val interp : Structures.constr -> btype -> Structures.constr -val interp_to_coq : reify_tbl -> btype -> Term.constr +val interp_to_coq : reify_tbl -> btype -> Structures.constr -val get_cuts : reify_tbl -> (Structures.names_id * Term.types) list +val get_cuts : reify_tbl -> (Structures.id * Structures.types) list val logic : btype -> logic |