diff options
| author | gareuselesinge | 2013-07-29 13:56:08 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-07-29 13:56:08 +0000 |
| commit | 5b012a717082f443a383b081eb5df5a3ee45be31 (patch) | |
| tree | e6f879e36d3ef31965e680b01eb5ec9971ad7944 | |
| parent | 1a53e944af3ae7a2c3fff695a1869b652d9ac5b7 (diff) | |
Revert "Only arguments declared as implicit can be renamed"
This reverts commit 18a89c271d540d794d44e41f50587bb1cad69802.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16640 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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) |