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/indtypes.ml | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

(limited to 'kernel/indtypes.ml')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 0f9c7421f3..85d04e5e24 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -195,11 +195,11 @@ let is_impredicative env u =
 
 let param_ccls params =
   let has_some_univ u = function
-    | Some v when Universe.equal u v -> true
+    | Some v when Univ.Level.equal u v -> true
     | _ -> false
   in
   let remove_some_univ u = function
-    | Some v when Universe.equal u v -> None
+    | Some v when Univ.Level.equal u v -> None
     | x -> x
   in
   let fold l (_, b, p) = match b with
@@ -210,10 +210,13 @@ let param_ccls params =
     (* polymorphism unless there is aliasing (i.e. non distinct levels) *)
     begin match kind_of_term c with
     | Sort (Type u) ->
-      if List.exists (has_some_univ u) l then
-        None :: List.map (remove_some_univ u) l
-      else
-        Some u :: l
+      (match Univ.Universe.level u with
+      | Some u ->
+	if List.exists (has_some_univ u) l then
+          None :: List.map (remove_some_univ u) l
+	else
+          Some u :: l
+      | None -> None :: l)
     | _ ->
       None :: l
     end
-- 
cgit v1.2.3