diff options
| author | gareuselesinge | 2011-12-19 16:18:20 +0000 |
|---|---|---|
| committer | gareuselesinge | 2011-12-19 16:18:20 +0000 |
| commit | 424a659278e15174e3829b965bb2118440748885 (patch) | |
| tree | e8284999acc35c6589421f9afdc7e9ca43eb87f3 | |
| parent | 92b6b2240392cc5a383fe76c3b19f4e4c7ae6c8f (diff) | |
Arguments: check rename even if no implicit is specified
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14827 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Arguments_renaming.v | 1 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 1 |
3 files changed, 4 insertions, 0 deletions
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 5de4ffd169..e443115cb3 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -1,5 +1,7 @@ The command has indeed failed with message: => Error: To rename arguments the "rename" flag must be specified. +The command has indeed failed with message: +=> Error: To rename arguments the "rename" flag must be specified. @eq_refl : forall (B : Type) (y : B), y = y eq_refl diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v index e9b5f247ec..b133e73355 100644 --- a/test-suite/output/Arguments_renaming.v +++ b/test-suite/output/Arguments_renaming.v @@ -1,4 +1,5 @@ Fail Arguments eq_refl {B y}, [B] y. +Fail Arguments identity T _ _. Arguments eq_refl A x. Arguments eq_refl {B y}, [B] y : rename. diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index b38c3bddc1..5787feb05d 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -809,6 +809,7 @@ let vernac_declare_arguments local r l nargs flags = error ("Argument "^string_of_id x^" cannot be declared implicit.") | (Name iid, _,_, true, max), Name id -> b || iid <> id, Some (ExplByName id, max, false) + | (Name iid, _,_, _, _), Name id -> b || iid <> id, None | _ -> b, None) sr (List.combine il inf_names) in sr || sr', Util.list_map_filter (fun x -> x) impl) |