aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
authorMaxime Dénès2018-09-11 10:23:02 +0200
committerMaxime Dénès2018-10-02 16:33:58 +0200
commitba63f39be8e26e04e94d1db7fcc534ad5f732871 (patch)
treee2ba13e46bed7fd6377c39d6e67a3baa140e177a /test-suite
parent7803262696980e6f2cb1fd4397b91f1098712647 (diff)
Revert #6651: Use r.(p) syntax to print primitive projections
Fixes #6764: Printing Notation regressed compared to 8.7
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/output/UnivBinders.out2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index f8f11d7cf6..1e50ba511a 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -5,7 +5,7 @@ PWrap has primitive projections with eta conversion.
For PWrap: Argument scope is [type_scope]
For pwrap: Argument scopes are [type_scope _]
punwrap@{u} =
-fun (A : Type@{u}) (p : PWrap@{u} A) => p.(punwrap)
+fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p
: forall A : Type@{u}, PWrap@{u} A -> A
(* u |= *)