diff options
| author | Gaëtan Gilbert | 2019-04-08 16:00:53 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-04-08 16:00:53 +0200 |
| commit | e9738ee2d21a84fc946d168aeaa68b169b309fd8 (patch) | |
| tree | b4b30d32deb6255b16b750db6459533618e3f7e6 /pretyping/reductionops.ml | |
| parent | 70a00b72035be1f5c3900a78df97d7350cc70bb6 (diff) | |
Don't store closures in summary (reduction effects)
We already have indirection (constant -> effect name, effect name ->
function) so we only need to stop using summary.ref for the second map.
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 71fbfe8716..1871609e18 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -53,7 +53,7 @@ type effect_name = string let constant_effect_table = Summary.ref ~name:"reduction-side-effect" Cmap.empty (* Table bindings function key to effective functions *) -let effect_table = Summary.ref ~name:"reduction-function-effect" String.Map.empty +let effect_table = ref String.Map.empty (** a test to know whether a constant is actually the effect function *) let reduction_effect_hook env sigma con c = |