aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--contrib/extraction/common.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 35dfd4d042..be68910870 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -64,8 +64,6 @@ module MonoParams = struct
let globals () = ! global_ids
- let cache r f = f r
-
let rename_global_id id =
let id' = rename_id id !global_ids in
global_ids := Idset.add id' !global_ids;