From e9738ee2d21a84fc946d168aeaa68b169b309fd8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 8 Apr 2019 16:00:53 +0200 Subject: [PATCH] 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. --- pretyping/reductionops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 71fbfe87162a..1871609e18cf 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 =