From 164c6861860e6b52818c031f901ffeff91fca16a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 26 Jan 2016 16:56:33 +0100
Subject: Imported Upstream version 8.5

---
 library/universes.ml | 24 +++++++++++++++---------
 1 file changed, 15 insertions(+), 9 deletions(-)

(limited to 'library/universes.ml')

diff --git a/library/universes.ml b/library/universes.ml
index 6cccb10e..7972c478 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -205,7 +205,7 @@ let leq_constr_univs_infer univs m n =
       else 
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
 	  if Univ.check_leq univs u1 u2 then
-	    ((if Univ.is_small_univ u1 then
+	    ((if Univ.is_type0_univ u1 then
 		cstrs := Constraints.add (u1, ULe, u2) !cstrs);
 	     true)
 	  else
@@ -820,7 +820,7 @@ let minimize_univ_variables ctx us algs left right cstrs =
 	    let cstrs' = List.fold_left (fun cstrs (d, r) -> 
 	      if d == Univ.Le then
 		enforce_leq inst (Universe.make r) cstrs
-	      else 
+	      else
 		try let lev = Option.get (Universe.level inst) in
 		      Constraint.add (lev, d, r) cstrs
 		with Option.IsNone -> failwith "")
@@ -854,7 +854,7 @@ let normalize_context_set ctx us algs =
     Constraint.fold (fun (l,d,r as cstr) (smallles, noneqs) ->
         if d == Le then
 	  if Univ.Level.is_small l then
-	    if is_set_minimization () then
+	    if is_set_minimization () && LSet.mem r ctx then
 	      (Constraint.add cstr smallles, noneqs)
 	    else (smallles, noneqs)
 	  else if Level.is_small r then
@@ -904,22 +904,28 @@ let normalize_context_set ctx us algs =
   let noneqs = Constraint.union noneqs smallles in
   let partition = UF.partition uf in
   let flex x = LMap.mem x us in
-  let ctx, subst, eqs = List.fold_left (fun (ctx, subst, cstrs) s -> 
+  let ctx, subst, us, eqs = List.fold_left (fun (ctx, subst, us, cstrs) s -> 
     let canon, (global, rigid, flexible) = choose_canonical ctx flex algs s in
     (* Add equalities for globals which can't be merged anymore. *)
     let cstrs = LSet.fold (fun g cst -> 
       Constraint.add (canon, Univ.Eq, g) cst) global
       cstrs 
     in
+    (* Also add equalities for rigid variables *)
+    let cstrs = LSet.fold (fun g cst -> 
+      Constraint.add (canon, Univ.Eq, g) cst) rigid
+      cstrs
+    in
     let subst = LSet.fold (fun f -> LMap.add f canon) rigid subst in
-    let subst = LSet.fold (fun f -> LMap.add f canon) flexible subst in 
-      (LSet.diff (LSet.diff ctx rigid) flexible, subst, cstrs))
-    (ctx, LMap.empty, Constraint.empty) partition
+    let subst = LSet.fold (fun f -> LMap.add f canon) flexible subst in
+    let canonu = Some (Universe.make canon) in
+    let us = LSet.fold (fun f -> LMap.add f canonu) flexible us in
+      (LSet.diff ctx flexible, subst, us, cstrs))
+    (ctx, LMap.empty, us, Constraint.empty) partition
   in
   (* Noneqs is now in canonical form w.r.t. equality constraints, 
      and contains only inequality constraints. *)
   let noneqs = subst_univs_level_constraints subst noneqs in
-  let us = LMap.fold (fun u v acc -> LMap.add u (Some (Universe.make v)) acc) subst us in
   (* Compute the left and right set of flexible variables, constraints
      mentionning other variables remain in noneqs. *)
   let noneqs, ucstrsl, ucstrsr = 
-- 
cgit v1.2.3