summaryrefslogtreecommitdiff
path: root/test-suite/output/ArgumentsScope.out
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/output/ArgumentsScope.out')
-rw-r--r--test-suite/output/ArgumentsScope.out5
1 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out
index 6643c142..756e8ede 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