Minor fixes from Gregory Malecha. A typo fixed and a better (located)

error message in case of unnammed record parameters.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13635 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 9 insertions, 0 deletions

diff --git a/toplevel/record.ml b/toplevel/record.ml
index d67c022a1e..fce531a31b 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -57,6 +57,15 @@ let binders_of_decls = List.map binder_of_decl
 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")
+    in
+      List.iter 
+	(function LocalRawDef (b, _) -> error b
+	   | LocalRawAssum (ls, _, ce) -> List.iter error 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
   let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in