diff options
Diffstat (limited to 'plugins/extraction/modutil.ml')
| -rw-r--r-- | plugins/extraction/modutil.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index bd48311308..60fe8e7620 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -8,7 +8,7 @@ open Names open Globnames -open Errors +open CErrors open Util open Miniml open Table @@ -310,7 +310,7 @@ let base_r = function let reset_needed, add_needed, add_needed_mp, found_needed, is_needed = let needed = ref Refset'.empty and needed_mps = ref MPset.empty in - ((fun l -> needed := Refset'.empty; needed_mps := MPset.empty), + ((fun () -> needed := Refset'.empty; needed_mps := MPset.empty), (fun r -> needed := Refset'.add (base_r r) !needed), (fun mp -> needed_mps := MPset.add mp !needed_mps), (fun r -> needed := Refset'.remove (base_r r) !needed), |