diff options
| author | Quentin Garchery <garchery.quentin@gmail.com> | 2018-10-27 18:08:53 +0200 |
|---|---|---|
| committer | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2018-10-27 18:29:50 +0200 |
| commit | 4e6129afb9aab53d14f16ac74a5a4e80323b5813 (patch) | |
| tree | 7037708e3ae50407842b8216117d0edb47e71c60 /src/trace/smtAtom.mli | |
| parent | a2e8b2f68fa82ca96468cb0613710c07b27192da (diff) | |
| download | smtcoq-4e6129afb9aab53d14f16ac74a5a4e80323b5813.tar.gz smtcoq-4e6129afb9aab53d14f16ac74a5a4e80323b5813.zip | |
formatting
Diffstat (limited to 'src/trace/smtAtom.mli')
| -rw-r--r-- | src/trace/smtAtom.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli index cdcdcd1..e6a3c47 100644 --- a/src/trace/smtAtom.mli +++ b/src/trace/smtAtom.mli @@ -142,8 +142,8 @@ 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 -> reify_tbl -> - Environ.env -> Evd.evar_map -> Term.constr -> t + val of_coq : Btype.reify_tbl -> Op.reify_tbl -> + reify_tbl -> Environ.env -> Evd.evar_map -> Term.constr -> t val to_coq : hatom -> Term.constr @@ -157,6 +157,7 @@ module Atom : (* Generation of atoms *) val hatom_Z_of_int : reify_tbl -> int -> hatom val hatom_Z_of_bigint : reify_tbl -> Big_int.big_int -> hatom + val mk_eq : reify_tbl -> btype -> hatom -> hatom -> hatom val mk_lt : reify_tbl -> hatom -> hatom -> hatom val mk_le : reify_tbl -> hatom -> hatom -> hatom |