From d9ac4c22a3a6543959d413120304e356d625c0f9 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 23 Jun 2015 15:40:16 +0200
Subject: Fix bug #4254 with the help of J.H. Jourdan

1) We now _assign_ the smallest possible arities to mutual inductive types
and eventually add leq constraints on the user given arities. Remove
useless limitation on instantiating algebraic universe variables with
their least upper bound if they have upper constraints as well.

2) Do not remove non-recursive variables when computing minimal levels of inductives.

3) Avoid modifying user-given arities if not necessary to compute the
minimal level of an inductive.

4) We correctly solve the recursive equations taking into account the
user-declared level.
---
 pretyping/evd.ml | 16 +++++++++++-----
 1 file changed, 11 insertions(+), 5 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 60b1da7049..168a10df93 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -351,10 +351,7 @@ let evar_universe_context_of ctx = { empty_evar_universe_context with uctx_local
 let evar_universe_context_subst ctx = ctx.uctx_univ_variables
 
 let instantiate_variable l b v =
-  (* let b = Univ.subst_large_constraint (Univ.Universe.make l) Univ.type0m_univ b in *)
-  (* if Univ.univ_depends (Univ.Universe.make l) b then  *)
-  (*   error ("Occur-check in universe variable instantiation") *)
-  (* else *) v := Univ.LMap.add l (Some b) !v
+  v := Univ.LMap.add l (Some b) !v
 
 exception UniversesDiffer
 
@@ -420,7 +417,16 @@ let process_universe_constraints univs vars alg cstrs =
 		      raise UniversesDiffer
 	      in
 	        Univ.enforce_eq_level l' r' local
-           | _, _ (* One of the two is algebraic or global *) -> 
+	    | Inr (l, loc, alg), Inl r
+	    | Inl r, Inr (l, loc, alg) ->
+	       let inst = Univ.univ_level_rem l r r in
+		 if alg then (instantiate_variable l inst vars; local)
+		 else
+		   let lu = Univ.Universe.make l in
+		   if Univ.univ_level_mem l r then
+		     Univ.enforce_leq inst lu local
+		   else raise (Univ.UniverseInconsistency (Univ.Eq, lu, r, None))
+            | _, _ (* One of the two is algebraic or global *) -> 
 	     if Univ.check_eq univs l r then local
 	     else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
   in
-- 
cgit v1.2.3


From 02663c526a3fd347fad803eb664d22e6b5c088ad Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sun, 28 Jun 2015 15:23:00 +0200
Subject: Fix incompleteness of conversion used by evarconv

In case we need to backtrack on universe inconsistencies when converting
two (incompatible) instances of the same constant and unfold them.
Bug reported by Amin Timany.
---
 pretyping/reductionops.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index dd671f111e..dc70f36ccf 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1287,7 +1287,9 @@ let sigma_compare_sorts env pb s0 s1 sigma =
     
 let sigma_compare_instances flex i0 i1 sigma =
   try Evd.set_eq_instances ~flex sigma i0 i1
-  with Evd.UniversesDiffer -> raise Reduction.NotConvertible
+  with Evd.UniversesDiffer
+     | Univ.UniverseInconsistency _ ->
+	raise Reduction.NotConvertible
 
 let sigma_univ_state = 
   { Reduction.compare = sigma_compare_sorts;
-- 
cgit v1.2.3