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 /test-suite | |
| 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
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Arguments_renaming.v | 1 |
2 files changed, 3 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. |