Statically enforce that ULub is only between levels.

2 files changed, 21 insertions, 10 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index f9cf5f6d8..53f6e28a9 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -700,18 +700,25 @@ let reducible_mind_case sigma c = match EConstr.kind sigma c with
 let magicaly_constant_of_fixbody env sigma reference bd = function
   | Name.Anonymous -> bd
   | Name.Name id ->
+    let open Universes in
     try
       let (cst_mod,cst_sect,_) = Constant.repr3 reference in
       let cst = Constant.make3 cst_mod cst_sect (Label.of_id id) in
-      let (cst, u), ctx = Universes.fresh_constant_instance env cst in
+      let (cst, u), ctx = fresh_constant_instance env cst in
       match constant_opt_value_in env (cst,u) with
       | None -> bd
       | Some t ->
         let csts = EConstr.eq_constr_universes env sigma (EConstr.of_constr t) bd in
         begin match csts with
         | Some csts ->
-          let subst = Universes.Constraints.fold (fun (l,d,r) acc ->
-            Univ.LMap.add (Option.get (Universe.level l)) (Option.get (Universe.level r)) acc)
+          let subst = Constraints.fold (fun cst acc ->
+              let l, r = match cst with
+                | ULub (u, v) -> u, v
+                | UEq (u, v) | ULe (u, v) ->
+                  let get u = Option.get (Universe.level u) in
+                  get u, get v
+              in
+            Univ.LMap.add l r acc)
             csts Univ.LMap.empty
           in
           let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 1cd8d3940..76bd88cc0 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -561,12 +561,16 @@ let is_rigid_head sigma flags t =
     | Lambda (_, _, _) | LetIn (_, _, _, _) | App (_, _) | Case (_, _, _, _)
     | Proj (_, _) -> false (* Why aren't Prod, Sort rigid heads ? *)
 
-let force_eqs c = 
-  Universes.Constraints.fold
-    (fun ((l,d,r) as c) acc -> 
-      let c' = if d == Universes.ULub then (l,Universes.UEq,r) else c in
-	Universes.Constraints.add c' acc) 
-    c Universes.Constraints.empty
+let force_eqs c =
+  let open Universes in
+  Constraints.fold
+    (fun c acc ->
+       let c' = match c with
+         | ULub (l, r) -> UEq (Univ.Universe.make l,Univ.Universe.make r)
+         | ULe _ | UEq _ -> c
+       in
+        Constraints.add c' acc)
+    c Constraints.empty
 
 let constr_cmp pb env sigma flags t u =
   let cstrs =
@@ -579,7 +583,7 @@ let constr_cmp pb env sigma flags t u =
       with Univ.UniverseInconsistency _ -> sigma, false
       | Evd.UniversesDiffer -> 
 	if is_rigid_head sigma flags t then 
-	  try Evd.add_universe_constraints sigma (force_eqs cstrs), true
+          try Evd.add_universe_constraints sigma (force_eqs cstrs), true
 	  with Univ.UniverseInconsistency _ -> sigma, false
 	else sigma, false
       end