Find a more efficient fix for dealing with template universes:

eagerly solve l <= k constraints as k := l when k is a fresh variable coming
from a template type. This has the effect of fixing the variable at the first
instantiation of the parameters of template polymorphic inductive and avoiding
to generate useless <= constraints that need to be minimized afterwards.

1 files changed, 8 insertions, 0 deletions

diff --git a/kernel/univ.ml b/kernel/univ.ml
index d931626e4..a9b511588 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -755,6 +755,10 @@ struct
 
     let pr x = str(to_string x)
 
+    let is_level = function
+      | (v, 0) -> true
+      | _ -> false
+
     let level = function
       | (v,0) -> Some v
       | _ -> None
@@ -809,6 +813,10 @@ struct
     | Cons (l, n) when is_nil n -> Some l
     | _ -> None
 
+  let is_level l = match node l with
+    | Cons (l, n) when is_nil n -> Expr.is_level l
+    | _ -> false
+
   let level l = match node l with
     | Cons (l, n) when is_nil n -> Expr.level l
     | _ -> None