From d6175b9980808ff91f1299ca26a9a49a117169ca Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 6 Apr 2017 17:34:23 +0200
Subject: Fix a normalization hotspot in computation of constr keys.

Getting a key only needs to observe the root of a term. This hotspot was
observed in HoTT.
---
 library/keys.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'library/keys.ml')

diff --git a/library/keys.ml b/library/keys.ml
index 057dc3b65d..c9e325ee57 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -114,11 +114,11 @@ let inKeys : key_obj -> obj =
 let declare_equiv_keys ref ref' =
   Lib.add_anonymous_leaf (inKeys (ref,ref'))
 
-let constr_key c =
+let constr_key kind c =
   let open Globnames in 
   try 
     let rec aux k = 
-      match kind_of_term k with
+      match kind k with
       | Const (c, _) -> KGlob (ConstRef c)
       | Ind (i, u) -> KGlob (IndRef i)
       | Construct (c,u) -> KGlob (ConstructRef c)
-- 
cgit v1.2.3