From e4ac6f91e8d95a168cdaeaec72cf761b7b6da4b7 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
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/constr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/constr.ml')

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
-- 
cgit v1.2.3