diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-08-10 11:16:37 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-08-10 11:16:37 +0200 |
| commit | 8d4df809c90352035f7bc92e1f829f2d482625ed (patch) | |
| tree | 76de63eb2cc4767e4205635f201376d5549287c1 /plugins/extraction/modutil.ml | |
| parent | 03bd49e69578665ae33e03300a1277b1c83e1939 (diff) | |
Make it a bit more obvious when variables are of type unit.
Diffstat (limited to 'plugins/extraction/modutil.ml')
| -rw-r--r-- | plugins/extraction/modutil.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 864d90a0f..60fe8e762 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -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), |