aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/tacred.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/tacred.ml')
-rw-r--r--pretyping/tacred.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 3563e9ca2..97ce40a77 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -124,9 +124,9 @@ type constant_evaluation =
(* We use a cache registered as a global table *)
-let eval_table = ref Cmap.empty
+type frozen = constant_evaluation Cmap.t
-type frozen = (int * constant_evaluation) Cmap.t
+let eval_table = ref (Cmap.empty : frozen)
let init () =
eval_table := Cmap.empty