diff options
| author | Quentin Garchery <garchery.quentin@gmail.com> | 2018-10-28 00:30:23 +0200 |
|---|---|---|
| committer | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2018-10-28 00:30:23 +0200 |
| commit | 7940ef63c654be26b41ce20162207f3c67d0b10a (patch) | |
| tree | 89d7e2a04b93a0cb37642416535637ddb45eba8b /src/trace/smtAtom.mli | |
| parent | cefda895d15a3f7eb7bf75402beb6fae22162585 (diff) | |
| download | smtcoq-7940ef63c654be26b41ce20162207f3c67d0b10a.tar.gz smtcoq-7940ef63c654be26b41ce20162207f3c67d0b10a.zip | |
New files SmtBtype.ml(i) for module formerly in SmtAtom
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 |