Fix (actually, properly implement :) hashconsing of projections,

resulting in huge speedup at Qed/section closing in presence of
primitive projections.

3 files changed, 19 insertions, 5 deletions

diff --git a/kernel/constr.ml b/kernel/constr.ml
index 0fd4c9d57..e757c5b56 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -821,7 +821,7 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
 	(Evar (e,l), combinesmall 8 (combine (Evar.hash e) hl))
       | Proj (p,c) ->
         let c, hc = sh_rec c in
-	let p' = Projection.hashcons p in
+	let p' = Projection.hcons p in
 	  (Proj (p', c), combinesmall 17 (combine (Projection.hash p') hc))
       | Const (c,u) ->
 	let c' = sh_con c in
diff --git a/kernel/names.ml b/kernel/names.ml
index 5d73bd520..13ea9e1d8 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'
diff --git a/kernel/names.mli b/kernel/names.mli
index 893cad09d..c71b76aab 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -645,7 +645,8 @@ module Projection : sig
 
   val equal : t -> t -> bool
   val hash : t -> int
-  val hashcons : t -> t
+  val hcons : t -> t
+  (** Hashconsing of projections. *)
 
   val compare : t -> t -> int