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/smtlib2/smtlib2_genConstr.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/smtlib2/smtlib2_genConstr.mli')
| -rw-r--r-- | src/smtlib2/smtlib2_genConstr.mli | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/smtlib2/smtlib2_genConstr.mli b/src/smtlib2/smtlib2_genConstr.mli index ba69741..1aa992e 100644 --- a/src/smtlib2/smtlib2_genConstr.mli +++ b/src/smtlib2/smtlib2_genConstr.mli @@ -2,16 +2,16 @@ val pp_symbol : Smtlib2_ast.symbol -> string val string_of_symbol : Smtlib2_ast.symbol -> string val identifier_of_qualidentifier : Smtlib2_ast.qualidentifier -> Smtlib2_ast.identifier -val string_type : string -> SmtAtom.btype -val sort_of_string : string -> SmtAtom.btype * 'a list -val sort_of_symbol : Smtlib2_ast.symbol -> SmtAtom.btype * 'a list +val string_type : string -> SmtBtype.btype +val sort_of_string : string -> SmtBtype.btype * 'a list +val sort_of_symbol : Smtlib2_ast.symbol -> SmtBtype.btype * 'a list val string_of_identifier : Smtlib2_ast.identifier -> string val string_of_qualidentifier : Smtlib2_ast.qualidentifier -> string -val sort_of_sort : Smtlib2_ast.sort -> (SmtAtom.btype * 'a list as 'a) +val sort_of_sort : Smtlib2_ast.sort -> (SmtBtype.btype * 'a list as 'a) val declare_sort : - SmtAtom.Btype.reify_tbl -> Smtlib2_ast.symbol -> SmtAtom.btype + SmtBtype.reify_tbl -> Smtlib2_ast.symbol -> SmtBtype.btype val declare_fun : - SmtAtom.Btype.reify_tbl -> + SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl -> Smtlib2_ast.symbol -> Smtlib2_ast.sort list -> Smtlib2_ast.sort -> SmtAtom.indexed_op @@ -22,13 +22,13 @@ val make_root : SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> Smtlib2_ast.term -> SmtAtom.Form.t val declare_commands : - SmtAtom.Btype.reify_tbl -> + SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl -> SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> SmtAtom.Form.t list -> Smtlib2_ast.command -> SmtAtom.Form.t list val import_smtlib2 : - SmtAtom.Btype.reify_tbl -> + SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl -> SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> string -> SmtAtom.Form.t list |