aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/Arguments_renaming.out
diff options
context:
space:
mode:
authorGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-11-03 23:33:12 +0000
committerGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-11-03 23:33:12 +0000
commit63eb223bc3cfdff1a985213a528c12728340323a (patch)
tree300bbc62d03e28619fafa2ea005c9abd5a3db98f /test-suite/output/Arguments_renaming.out
parenta904c15ef60c41a97300b0170208f2541f6adc7c (diff)
test-suite fixup
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17046 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/output/Arguments_renaming.out')
-rw-r--r--test-suite/output/Arguments_renaming.out6
1 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index bdf0a0cf8..5273c59ec 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -1,9 +1,9 @@
The command has indeed failed with message:
=> Error: To rename arguments the "rename" flag must be specified.
-Argument A renamed to B
+Argument A renamed to B.
The command has indeed failed with message:
=> Error: To rename arguments the "rename" flag must be specified.
-Argument A renamed to T
+Argument A renamed to T.
@eq_refl
: forall (B : Type) (y : B), y = y
eq_refl
@@ -110,4 +110,4 @@ The command has indeed failed with message:
=> Error: Extra argument y.
The command has indeed failed with message:
=> Error: To rename arguments the "rename" flag must be specified.
-Argument A renamed to R
+Argument A renamed to R.