diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-19 16:18:20 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-19 16:18:20 +0000 |
| commit | 424a659278e15174e3829b965bb2118440748885 (patch) | |
| tree | e8284999acc35c6589421f9afdc7e9ca43eb87f3 /test-suite/output/Arguments_renaming.out | |
| 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/output/Arguments_renaming.out')
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 5de4ffd16..e443115cb 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 |