diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-06 16:02:07 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-06 16:02:07 +0000 |
| commit | 5e1b9c5e895938774253891ec8121be3d713e793 (patch) | |
| tree | ac3fade5b4134bc22e252b1c4334f0ccb0a943d1 /test-suite/output/Arguments_renaming.out | |
| parent | c4d9efb1d6cca48fd33764fa1f17172d86b13e78 (diff) | |
Minor fixes to Arguments
- Implicit arguments can be mentioned anonymously:
Arguments map {_ _} f l.
- To rename implicit arguments, the ": rename" flag must be used:
Arguments map {T1 T2} f l : rename.
Without the ": rename" flag arguments can be used to assert
that a function has indeed the expected number of arguments and
that the arguments are named as expected.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14766 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/output/Arguments_renaming.out')
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index ed08334e7..925ff693a 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -1,3 +1,5 @@ +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 @@ -99,6 +101,6 @@ The command has indeed failed with message: The command has indeed failed with message: => Error: Arguments names must be distinct The command has indeed failed with message: -=> Error: Argument z is anonymous and cannot be declared implicit +=> Error: Argument z cannot be declared implicit The command has indeed failed with message: => Error: Extra argument y |