aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--pretyping/reductionops.ml2
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 =