From a8ee1bef887fbf14ffe1380152993b0db4298c98 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 9 May 2014 03:04:35 +0200
Subject: Reuse universe level substitutions for template polymorphism, fixing
 performance problem with hashconsing at the same time. This fixes bug# 3302.

---
 kernel/typeops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/typeops.ml')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index c6355b3eab..49f883628d 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -115,7 +115,7 @@ let check_hyps_inclusion env c sign =
 
 let extract_level env p =
   let _,c = dest_prod_assum env p in
-  match kind_of_term c with Sort (Type u) -> Some u | _ -> None
+  match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None
 
 let extract_context_levels env l =
   let fold l (_, b, p) = match b with
-- 
cgit v1.2.3