From 16cf970765096f55a03efad96100add581ce0edb Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 18 Nov 2010 17:37:59 +0000
Subject: Do not throw an error for anonymous generalized binders as they will
 be named after interpretation.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13650 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/record.ml | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

diff --git a/toplevel/record.ml b/toplevel/record.ml
index fce531a31b..707e0dc4a9 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -58,13 +58,16 @@ let typecheck_params_and_fields id t ps nots fs =
   let env0 = Global.env () in
   let evars = ref Evd.empty in
   let _ = 
-    let error (loc, name) = 
-      if name = Anonymous then 
-	user_err_loc (loc, "record", str "Record parameters must be named")
+    let error bk (loc, name) = 
+      match bk with
+      | Default _ ->
+	  if name = Anonymous then 
+	    user_err_loc (loc, "record", str "Record parameters must be named")
+      | _ -> ()
     in
       List.iter 
-	(function LocalRawDef (b, _) -> error b
-	   | LocalRawAssum (ls, _, ce) -> List.iter error ls) ps
+	(function LocalRawDef (b, _) -> error default_binder_kind b
+	   | LocalRawAssum (ls, bk, ce) -> List.iter (error bk) ls) ps
   in 
   let (env1,newps), imps = interp_context_evars evars env0 ps in
   let fullarity = it_mkProd_or_LetIn (Option.cata (fun x -> x) (Termops.new_Type ()) t) newps in
-- 
cgit v1.2.3