diff options
| author | ckeller <ckeller@users.noreply.github.com> | 2021-04-21 10:59:23 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-21 10:59:23 +0200 |
| commit | 9dbc62938011b07ae28795cdc7e2f8ddea01ef2a (patch) | |
| tree | 1e50ed6dcba7213a9b1340e5e8e45042e6f67715 /src/trace/smtMisc.mli | |
| parent | 4a2ef2747950e8a28bfce7ca641bedd7ef71bea1 (diff) | |
| download | smtcoq-9dbc62938011b07ae28795cdc7e2f8ddea01ef2a.tar.gz smtcoq-9dbc62938011b07ae28795cdc7e2f8ddea01ef2a.zip | |
Warning (instead of error) for unsupported lemmas (#90)
Diffstat (limited to 'src/trace/smtMisc.mli')
| -rw-r--r-- | src/trace/smtMisc.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/trace/smtMisc.mli b/src/trace/smtMisc.mli index f3bcf60..e442e68 100644 --- a/src/trace/smtMisc.mli +++ b/src/trace/smtMisc.mli @@ -19,3 +19,6 @@ val string_coq_constr : Structures.constr -> string type logic_item = LUF | LLia | LBitvectors | LArrays module SL : Set.S with type elt = logic_item type logic = SL.t + +(** Utils *) +val filter_map : ('a -> 'b option) -> 'a list -> 'b list |