From e4ac6f91e8d95a168cdaeaec72cf761b7b6da4b7 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 17 Dec 2014 18:36:24 +0100
Subject: Fix (actually, properly implement :) hashconsing of projections,
 resulting in huge speedup at Qed/section closing in presence of primitive
 projections.

---
 kernel/names.ml | 19 ++++++++++++++++---
 1 file changed, 16 insertions(+), 3 deletions(-)

(limited to 'kernel/names.ml')

diff --git a/kernel/names.ml b/kernel/names.ml
index 5d73bd5209..13ea9e1d86 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -794,10 +794,23 @@ struct
   let unfolded = snd
   let unfold (c, b as p) = if b then p else (c, true)
   let equal (c, b) (c', b') = Constant.equal c c' && b == b'
+
   let hash (c, b) = (if b then 0 else 1) + Constant.hash c
-  let hashcons (c, b as x) = 
-    let c' = hcons_con c in 
-      if c' == c then x else (c', b)
+
+  module Self_Hashcons =
+    struct
+      type _t = t
+      type t = _t
+      type u = Constant.t -> Constant.t
+      let hashcons hc (c,b) = (hc c,b)
+      let equal ((c,b) as x) ((c',b') as y) =
+        x == y || (c == c' && b == b')
+      let hash = hash
+    end
+
+  module HashProjection = Hashcons.Make(Self_Hashcons)
+
+  let hcons = Hashcons.simple_hcons HashProjection.generate hcons_con
 
   let compare (c, b) (c', b') =
     if b == b' then Constant.CanOrd.compare c c'
-- 
cgit v1.2.3