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/names.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'kernel/names.mli')

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