From c8dcfc691a649ff6dfb3416809c6ec7b1e629b1f Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 17 Mar 2016 20:23:00 +0100
Subject: Fix bug #4627: records with no declared arity can be template
 polymorphic.

As if we were adding : Type. Consistent with inductives with no
declared arity.
---
 toplevel/record.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/record.ml b/toplevel/record.ml
index 200d1a9387..c5ae7e8913 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -114,13 +114,13 @@ let typecheck_params_and_fields def id pl t ps nots fs =
 	 (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 (* (not def) *) l; 
+	   | Some l -> evars := Evd.make_flexible_variable !evars true l; 
 	     sred, true
 	   | None -> s, false)
 	 | _ -> user_err_loc (constr_loc t,"", str"Sort expected."))
     | None -> 
-      let uvarkind = if (* not def *) true then Evd.univ_flexible_alg else Evd.univ_flexible in
-	mkSort (Evarutil.evd_comb0 (Evd.new_sort_variable uvarkind) evars), false
+      let uvarkind = Evd.univ_flexible_alg in
+	mkSort (Evarutil.evd_comb0 (Evd.new_sort_variable uvarkind) evars), true
   in
   let fullarity = it_mkProd_or_LetIn t' newps in
   let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in
-- 
cgit v1.2.3