diff options
Diffstat (limited to 'src/trace/smtAtom.mli')
-rw-r--r-- | src/trace/smtAtom.mli | 43 |
1 files changed, 3 insertions, 40 deletions
diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli index e6a3c47..8e69265 100644 --- a/src/trace/smtAtom.mli +++ b/src/trace/smtAtom.mli @@ -13,44 +13,7 @@ (* *) (**************************************************************************) - -type indexed_type - -val dummy_indexed_type: int -> indexed_type -val indexed_type_index : indexed_type -> int - -type btype = - | TZ - | Tbool - | Tpositive - | Tindex of indexed_type - -module Btype : - sig - - val equal : btype -> btype -> bool - - val to_coq : btype -> Term.constr - - val to_smt : Format.formatter -> btype -> unit - - type reify_tbl - - val create : unit -> reify_tbl - - val declare : reify_tbl -> Term.constr -> Term.constr -> btype - - val of_coq : reify_tbl -> Term.constr -> btype - - val interp_tbl : reify_tbl -> Term.constr - - val to_list : reify_tbl -> (int * indexed_type) list - - val interp_to_coq : reify_tbl -> btype -> Term.constr - - val get_cuts : reify_tbl -> (Structures.names_id_t * Term.types) list - - end +open SmtBtype (** Operators *) @@ -142,7 +105,7 @@ module Atom : val get : reify_tbl -> atom -> hatom (** Given a coq term, build the corresponding atom *) - val of_coq : Btype.reify_tbl -> Op.reify_tbl -> + val of_coq : SmtBtype.reify_tbl -> Op.reify_tbl -> reify_tbl -> Environ.env -> Evd.evar_map -> Term.constr -> t val to_coq : hatom -> Term.constr @@ -178,5 +141,5 @@ module Trace : sig end -val make_t_i : Btype.reify_tbl -> Term.constr +val make_t_i : SmtBtype.reify_tbl -> Term.constr val make_t_func : Op.reify_tbl -> Term.constr -> Term.constr |