aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/output/Arguments.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v
index 97df40f882..844f96aaa1 100644
--- a/test-suite/output/Arguments.v
+++ b/test-suite/output/Arguments.v
@@ -51,7 +51,7 @@ Arguments pi _ _%F _%B.
Check (forall w : r, pi w $ $ = tt).
Fail Check (forall w : r, w $ $ = tt).
Axiom w : r.
-Arguments w _%F _%B : extra scopes.
+Arguments w x%F y%B : extra scopes.
Check (w $ $ = tt).
Fail Arguments w _%F _%B.