aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/ArgumentsScope.out
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-12-04 20:48:26 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-12-04 20:48:26 +0000
commit7d3ca4346465f31bd58ead06b9856637c0f5fc4d (patch)
tree19d1494778ad94377b02e833bf7f4f16ceae499d /test-suite/output/ArgumentsScope.out
parent17e99469c656a157f5ab998e21c41294ea2abbf8 (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/ArgumentsScope.out')
-rw-r--r--test-suite/output/ArgumentsScope.out10
1 files changed, 5 insertions, 5 deletions
diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out
index c95f89c9f..756e8ede9 100644
--- a/test-suite/output/ArgumentsScope.out
+++ b/test-suite/output/ArgumentsScope.out
@@ -21,6 +21,11 @@ negb : bool -> bool
Argument scope is [bool_scope]
negb is transparent
Expands to: Constant Coq.Init.Datatypes.negb
+Warning: Arguments Scope is deprecated; use Arguments instead
+Warning: Arguments Scope is deprecated; use Arguments instead
+Warning: Arguments Scope is deprecated; use Arguments instead
+Warning: Arguments Scope is deprecated; use Arguments instead
+Warning: Arguments Scope is deprecated; use Arguments instead
a : bool -> bool
Expands to: Variable a
@@ -54,8 +59,3 @@ negb'' : bool -> bool
negb'' is transparent
Expands to: Constant Top.negb''
-Warning: Arguments Scope is deprecated; use Arguments instead
-Warning: Arguments Scope is deprecated; use Arguments instead
-Warning: Arguments Scope is deprecated; use Arguments instead
-Warning: Arguments Scope is deprecated; use Arguments instead
-Warning: Arguments Scope is deprecated; use Arguments instead