Reuse universe level substitutions for template polymorphism, fixing performance

problem with hashconsing at the same time. This fixes bug# 3302.

1 files changed, 9 insertions, 6 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 0f9c7421f..85d04e5e2 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