From 23d30ddc2a7cdfa3f71e99f57d36818b16ad40b7 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 3 Jul 2014 23:45:01 +0200
Subject: Cleanup code related to the constraint solving, which sits now
 outside the kernel in library/universes.ml.

---
 pretyping/inductiveops.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'pretyping/inductiveops.ml')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 07a3378363..313bf6110c 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -480,13 +480,13 @@ let rec instantiate_universes env evdref scl is = function
       d :: instantiate_universes env evdref scl is (sign, exp)
   | d::sign, None::exp ->
       d :: instantiate_universes env evdref scl is (sign, exp)
-  | (na,None,ty)::sign, Some u::exp ->
+  | (na,None,ty)::sign, Some l::exp ->
       let ctx,_ = Reduction.dest_arity env ty in
-      let u = Univ.Universe.make u in
+      let u = Univ.Universe.make l in
       let s =
 	(* Does the sort of parameter [u] appear in (or equal)
            the sort of inductive [is] ? *)
-        if univ_depends u is then
+        if univ_level_mem l is then
           scl (* constrained sort: replace by scl *)
         else
           (* unconstrained sort: replace by fresh universe *)
-- 
cgit v1.2.3