diff options
| author | Hugo Herbelin | 2019-11-14 08:26:14 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-22 22:37:15 +0100 |
| commit | 14196d8ab425f67faf3995bd29a003de3b2e87ac (patch) | |
| tree | 37379c35029ee6269a9796f42f360e329b4f9a23 /test-suite/output | |
| parent | 556e9dde62b6822db20bd5c7e6e6a67bc717c408 (diff) | |
Propagate implicit arguments in all notations for partial applications.
This was done for abbreviations but not string notations. This adopts
the policy proposed in #11091 to make parsing and printing consistent.
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/Notations5.out | 12 | ||||
| -rw-r--r-- | test-suite/output/Notations5.v | 20 |
2 files changed, 18 insertions, 14 deletions
diff --git a/test-suite/output/Notations5.out b/test-suite/output/Notations5.out index 990a7151b4..9b50b53456 100644 --- a/test-suite/output/Notations5.out +++ b/test-suite/output/Notations5.out @@ -226,8 +226,10 @@ where : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b ## 0 : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b -@p nat 0 0 - : forall (B : Type) (b : B), 0 = 0 /\ b = b +## 0 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] ## 0 0 (B:=bool) : forall b : bool, 0 = 0 /\ b = b ## 0 0 (B:=bool) @@ -240,8 +242,10 @@ where : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b ## 0 : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b -@p nat 0 0 - : forall (B : Type) (b : B), 0 = 0 /\ b = b +## 0 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] ## 0 0 (B:=bool) : forall b : bool, 0 = 0 /\ b = b ## 0 0 (B:=bool) diff --git a/test-suite/output/Notations5.v b/test-suite/output/Notations5.v index 0b78c388fa..49378ab846 100644 --- a/test-suite/output/Notations5.v +++ b/test-suite/output/Notations5.v @@ -299,15 +299,15 @@ Module AppliedTermsPrinting. Check ## 0. (* ## 0 *) Check ## 0 0. - (* @p nat 0 0 *) + (* ## 0 0 *) Check p 0 0 (B:=bool). (* ## 0 0 (B:=bool) *) - Check ## 0 0 bool. - (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *) + Check ## 0 0 (B:=bool). + (* ## 0 0 (B:=bool) *) Check p 0 0 true. (* ## 0 0 true *) - Check ## 0 0 bool true. - (* ## 0 0 true -- INCONSISTENT parsing/printing *) + Check ## 0 0 true. + (* ## 0 0 true *) End NotationForPartialApplication. @@ -325,15 +325,15 @@ Module AppliedTermsPrinting. Check ## 0. (* ## 0 *) Check ## 0 0. - (* @p nat 0 0 *) + (* ## 0 0 *) Check p 0 0 (B:=bool). (* ## 0 0 (B:=bool) *) - Check ## 0 0 bool. - (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *) + Check ## 0 0 (B:=bool). + (* ## 0 0 (B:=bool) *) Check p 0 0 true. (* ## 0 0 true *) - Check ## 0 0 bool true. - (* ## 0 0 true -- INCONSISTENCY parsing/printing *) + Check ## 0 0 true. + (* ## 0 0 true *) End AtNotationForPartialApplication. |