diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Notations5.out | 4 | ||||
| -rw-r--r-- | test-suite/output/Notations5.v | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/test-suite/output/Notations5.out b/test-suite/output/Notations5.out index 96687ed07f..7afb5ad396 100644 --- a/test-suite/output/Notations5.out +++ b/test-suite/output/Notations5.out @@ -104,9 +104,9 @@ u : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b where ?A : [ |- Type] -u +@u : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b -u +@u : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b u : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b diff --git a/test-suite/output/Notations5.v b/test-suite/output/Notations5.v index 3c25547aac..92ac4b03ff 100644 --- a/test-suite/output/Notations5.v +++ b/test-suite/output/Notations5.v @@ -145,9 +145,9 @@ Module AppliedTermsPrinting. Check p. (* u *) Check @p. - (* u -- BUG *) + (* @u *) Check @u. - (* u -- BUG *) + (* @u *) Check u. (* u *) Check p 0 0. |