From 50237af2da42eca2b1f87569433f422ae409de39 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 28 Aug 2014 22:52:08 +0200
Subject: Fixing bug #3528.

---
 toplevel/command.ml | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'toplevel')

diff --git a/toplevel/command.ml b/toplevel/command.ml
index b10a4da06d..6d1ca685e0 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -454,8 +454,20 @@ let inductive_levels env evdref poly arities inds =
     !evdref (Array.to_list levels') destarities sizes
   in evdref := evd; arities
 
+let check_named (loc, na) = match na with
+| Name _ -> ()
+| Anonymous ->
+  let msg = str "Parameters must be named." in
+  user_err_loc (loc, "", msg)
+
+
+let check_param = function
+| LocalRawDef (na, _) -> check_named na
+| LocalRawAssum (nas, _, _) -> List.iter check_named nas
+
 let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
   check_all_names_different indl;
+  List.iter check_param paramsl;
   let env0 = Global.env() in
   let evdref = ref Evd.(from_env env0) in
   let _, ((env_params, ctx_params), userimpls) =
-- 
cgit v1.2.3