diff options
| author | gareuselesinge | 2013-04-18 08:48:25 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-04-18 08:48:25 +0000 |
| commit | ae1960c4fb1c65cd68fe39bc2f6d180682625d72 (patch) | |
| tree | 32a026a43b46ac5b703e29714118c27670ad72b0 | |
| parent | 1db7a2ab06f866cc20c0f29eb8b82577034b5378 (diff) | |
Only arguments declared as implicit can be renamed
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16427 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/vernacentries.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index a3aa6607e8..498c653ab0 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1007,7 +1007,11 @@ 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, _,_, _, _), Name id -> b || not (Id.equal iid id), None + | (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 | _ -> b, None) sr (List.combine il inf_names) in sr || sr', List.map_filter (fun x -> x) impl) |