summaryrefslogtreecommitdiff
path: root/libs
diff options
context:
space:
mode:
Diffstat (limited to 'libs')
-rw-r--r--libs/util.ml8
1 files changed, 8 insertions, 0 deletions
diff --git a/libs/util.ml b/libs/util.ml
new file mode 100644
index 0000000..b2838b6
--- /dev/null
+++ b/libs/util.ml
@@ -0,0 +1,8 @@
+
+module VarMap = Mapext.Make(String)
+
+let rec fix f s =
+ let fs = f s in
+ if fs = s
+ then fs
+ else fix f fs