diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-04 20:48:26 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-04 20:48:26 +0000 |
| commit | 7d3ca4346465f31bd58ead06b9856637c0f5fc4d (patch) | |
| tree | 19d1494778ad94377b02e833bf7f4f16ceae499d /test-suite/output/Implicit.v | |
| parent | 17e99469c656a157f5ab998e21c41294ea2abbf8 (diff) | |
Fixing superflous newline in output of About when no parameter is renamed.
Fixing output tests after having added flushing of warning in
revisions 14747 and 14750.
Moving Implicit output test to new command Arguments.
Adding test of new Arguments syntax in PrintInfos.v.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14758 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/output/Implicit.v')
| -rw-r--r-- | test-suite/output/Implicit.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/Implicit.v b/test-suite/output/Implicit.v index d50c98765..7c9b89f9d 100644 --- a/test-suite/output/Implicit.v +++ b/test-suite/output/Implicit.v @@ -36,7 +36,7 @@ Check map id (1::nil). Definition id' (A:Type) (x:A) := x. -Implicit Arguments id' [[A]]. +Arguments id' {A} x. Check map id' (1::nil). |