From 84290ba5da2a6acb4bf95b197f7a7ce8b072a1d0 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 29 Apr 2014 16:04:11 +0200
Subject: 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.

---
 kernel/univ.ml  | 8 ++++++++
 kernel/univ.mli | 3 +++
 2 files changed, 11 insertions(+)

(limited to 'kernel')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index d931626e4d..a9b5115886 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
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 20ee554f18..cc5eedefb5 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -118,6 +118,9 @@ sig
   val pr : t -> Pp.std_ppcmds
   (** Pretty-printing *)
 
+  val is_level : t -> bool
+  (** Test if the universe is a level or an algebraic universe. *)
+
   val level : t -> Level.t option
   (** Try to get a level out of a universe, returns [None] if it
       is an algebraic universe. *)
-- 
cgit v1.2.3