aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/Implicit.out
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/output/Implicit.out')
-rw-r--r--test-suite/output/Implicit.out2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out
index d8b88b8c1c..781e8e13a3 100644
--- a/test-suite/output/Implicit.out
+++ b/test-suite/output/Implicit.out
@@ -5,7 +5,7 @@ ex_intro (P:=fun _ : nat => True) (x:=0) I
d2 = fun x : nat => d1 (y:=x)
: forall x x0 : nat, x0 = x -> x0 = x
-Arguments d2 [x x]%nat_scope
+Arguments d2 [x x]%nat_scope _
map id (1 :: nil)
: list nat
map id' (1 :: nil)