From 8abdf84ad8cd82b7ea0e0b2adb97255b2f70fbb8 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 24 Sep 2015 15:20:15 +0200
Subject: Univs: correcly compute the levels of records when they fall in Prop.

---
 toplevel/record.ml | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/toplevel/record.ml b/toplevel/record.ml
index ee80101f3d..4a2bfaa8b0 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -131,14 +131,18 @@ let typecheck_params_and_fields def id pl t ps nots fs =
     Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar !evars (Evd.empty,!evars) in
   let evars, nf = Evarutil.nf_evars_and_universes sigma in
   let arity = nf t' in
-  let evars = 
+  let arity, evars = 
     let _, univ = compute_constructor_level evars env_ar newfs in
     let ctx, aritysort = Reduction.dest_arity env0 arity in
       assert(List.is_empty ctx); (* Ensured by above analysis *)
       if Sorts.is_prop aritysort || 
 	(Sorts.is_set aritysort && is_impredicative_set env0) then
-	evars
-      else Evd.set_leq_sort env_ar evars (Type univ) aritysort
+	arity, evars
+      else
+	let evars = Evd.set_leq_sort env_ar evars (Type univ) aritysort in
+	  if Univ.is_small_univ univ then
+	    mkArity (ctx, Sorts.sort_of_univ univ), evars
+	  else arity, evars
   in
   let evars, nf = Evarutil.nf_evars_and_universes evars in
   let newps = map_rel_context nf newps in
-- 
cgit v1.2.3