From 25ffe7f97a907d3508848c81c3e8dcc89559aadd Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 27 May 2016 13:51:51 +0200
Subject: Univs: earlier errors for strict univ decls #4527

When declaring the universes of a lemma explicitely, throw an error if
after minimization the type of a lemma still refers to unbound
universes. This is a fix and an incompatibility, but scripts
will be backwards compatible themselves.
Fix another minor bug in treating universe binders for (Co)Fixpoint.
---
 toplevel/command.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/command.ml b/toplevel/command.ml
index ffa2484eef..2875511d35 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1087,7 +1087,7 @@ let interp_recursive isfix fixl notations =
         | Some ls , Some us ->
 	   if not (CList.for_all2eq (fun x y -> Id.equal (snd x) (snd y)) ls us) then
 	     error "(co)-recursive definitions should all have the same universe binders";
-	   Some (ls @ us)) fixl None in
+	   Some us) fixl None in
   let ctx = Evd.make_evar_universe_context env all_universes in
   let evdref = ref (Evd.from_ctx ctx) in
   let fixctxs, fiximppairs, fixannots =
-- 
cgit v1.2.3


From c200c2b41e88dd7d4a1b9e90e0c35a7ed047309c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 30 May 2016 23:52:58 +0200
Subject: Univs: Fix bug #4726

When using Record and an explicit sort constraint, the
universe was wrongly made flexible and minimized.
---
 toplevel/record.ml | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/record.ml b/toplevel/record.ml
index 3151b13726..e9de6b5324 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -114,14 +114,19 @@ let typecheck_params_and_fields def id pl t ps nots fs =
   let t', template = match t with 
     | Some t -> 
        let env = push_rel_context newps env0 in
+       let poly =
+         match t with
+         | CSort (_, Misctypes.GType []) -> true | _ -> false in
        let s = interp_type_evars env evars ~impls:empty_internalization_env t in
        let sred = Reductionops.whd_betadeltaiota env !evars s in
 	 (match kind_of_term sred with
 	 | Sort s' -> 
-	   (match Evd.is_sort_variable !evars s' with
-	   | Some l -> evars := Evd.make_flexible_variable !evars true l; 
-	     sred, true
-	   | None -> s, false)
+	    (if poly then
+               match Evd.is_sort_variable !evars s' with
+	       | Some l -> evars := Evd.make_flexible_variable !evars true l; 
+	                  sred, true
+	       | None -> s, false
+             else s, false)
 	 | _ -> user_err_loc (constr_loc t,"", str"Sort expected."))
     | None -> 
       let uvarkind = Evd.univ_flexible_alg in
-- 
cgit v1.2.3