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/verit/veritSyntax.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/verit/veritSyntax.mli')
| -rw-r--r-- | src/verit/veritSyntax.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/verit/veritSyntax.mli b/src/verit/veritSyntax.mli index 281deef..c7bf659 100644 --- a/src/verit/veritSyntax.mli +++ b/src/verit/veritSyntax.mli @@ -31,8 +31,8 @@ val lit_of_atom_form_lit : SmtAtom.Form.reify -> atom_form_lit -> SmtAtom.Form.t val get_solver : int -> atom_form_lit val add_solver : int -> atom_form_lit -> unit -val get_btype : string -> SmtAtom.btype -val add_btype : string -> SmtAtom.btype -> unit +val get_btype : string -> SmtBtype.btype +val add_btype : string -> SmtBtype.btype -> unit val get_fun : string -> SmtAtom.indexed_op val add_fun : string -> SmtAtom.indexed_op -> unit |