diff options
| author | Pierre-Marie Pédrot | 2014-08-28 22:52:08 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-08-28 23:02:48 +0200 |
| commit | 50237af2da42eca2b1f87569433f422ae409de39 (patch) | |
| tree | c32521ceda090ddaa357476aac814315b0acc927 | |
| parent | 58543b45425b85233c068f9da859996270d1fdcf (diff) | |
Fixing bug #3528.
| -rw-r--r-- | toplevel/command.ml | 12 |
1 files changed, 12 insertions, 0 deletions
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) = |