aboutsummaryrefslogtreecommitdiffstats
path: root/src/trace/smtMisc.ml
diff options
context:
space:
mode:
authorChantal Keller <Chantal.Keller@lri.fr>2021-04-21 13:12:03 +0200
committerChantal Keller <Chantal.Keller@lri.fr>2021-04-21 13:12:03 +0200
commitf5db7098fae39f584550ed5dd03cac34dc24be67 (patch)
treedf0cef1808bf096049622faa9e2509756d7b4c2c /src/trace/smtMisc.ml
parent13d2c8be2ffb84bc8d40064b223562832e5a5a7e (diff)
parent9dbc62938011b07ae28795cdc7e2f8ddea01ef2a (diff)
downloadsmtcoq-f5db7098fae39f584550ed5dd03cac34dc24be67.tar.gz
smtcoq-f5db7098fae39f584550ed5dd03cac34dc24be67.zip
Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10
Diffstat (limited to 'src/trace/smtMisc.ml')
-rw-r--r--src/trace/smtMisc.ml6
1 files changed, 6 insertions, 0 deletions
diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml
index d33a0ec..0b6eeaa 100644
--- a/src/trace/smtMisc.ml
+++ b/src/trace/smtMisc.ml
@@ -50,3 +50,9 @@ module SL = Set.Make (struct
end)
type logic = SL.t
+
+
+(** Utils *)
+let rec filter_map f = function
+ | [] -> []
+ | x::xs -> match f x with Some x -> x::(filter_map f xs) | None -> filter_map f xs