diff options
| -rw-r--r-- | toplevel/vernacentries.ml | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index fbd81352f3..d583c4fe6f 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1002,11 +1002,7 @@ let vernac_declare_arguments locality r l nargs flags = error ("Argument "^Id.to_string x^" cannot be declared implicit.") | (Name iid, _,_, true, max), Name id -> b || not (Id.equal iid id), Some (ExplByName id, max, false) - | (Name iid, _,_, false, _), Name id -> - if not (Id.equal iid id) then - error("Argument "^Id.to_string id^" cannot be renamed to "^ - Id.to_string iid^" because it is not declared as implicit"); - b, None + | (Name iid, _,_, _, _), Name id -> b || not (Id.equal iid id), None | _ -> b, None) sr (List.combine il inf_names) in sr || sr', List.map_filter (fun x -> x) impl) |