From 42dd4e73346e29db2fe586234b00ca79bd207a5a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 30 Sep 2015 18:31:17 +0200
Subject: Univs: fix inference of the lowest sort for records.

---
 toplevel/record.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/toplevel/record.ml b/toplevel/record.ml
index 4a2bfaa8b0..60fe76bb82 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -141,7 +141,10 @@ let typecheck_params_and_fields def id pl t ps nots fs =
       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
+	    (* We can assume that the level aritysort is not constrained
+  	       and clear it. *)
+	    mkArity (ctx, Sorts.sort_of_univ univ),
+	    Evd.set_eq_sort env_ar evars (Prop Pos) aritysort
 	  else arity, evars
   in
   let evars, nf = Evarutil.nf_evars_and_universes evars in
-- 
cgit v1.2.3