diff options
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/Notations5.out | 20 | ||||
| -rw-r--r-- | test-suite/output/Notations5.v | 24 |
2 files changed, 24 insertions, 20 deletions
diff --git a/test-suite/output/Notations5.out b/test-suite/output/Notations5.out index c5b4d6f291..96687ed07f 100644 --- a/test-suite/output/Notations5.out +++ b/test-suite/output/Notations5.out @@ -138,7 +138,7 @@ v 0 : forall b : ?B, 0 = 0 /\ b = b where ?B : [ |- Type] -v 0 (B:=bool) true +v 0 true : 0 = 0 /\ true = true v : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b @@ -158,7 +158,7 @@ v 0 : forall b : ?B, 0 = 0 /\ b = b where ?B : [ |- Type] -v 0 (B:=bool) true +v 0 true : 0 = 0 /\ true = true v : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b @@ -188,9 +188,9 @@ where : forall b : ?B, 0 = 0 /\ b = b where ?B : [ |- Type] -## 0 0 (B:=bool) true +## 0 0 true : 0 = 0 /\ true = true -## 0 0 (B:=bool) true +## 0 0 true : 0 = 0 /\ true = true ## 0 0 (B:=bool) : forall b : bool, 0 = 0 /\ b = b @@ -226,23 +226,27 @@ p 0 0 true : 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 (B:=bool) : forall b : bool, 0 = 0 /\ b = b ## 0 0 (B:=bool) : forall b : bool, 0 = 0 /\ b = b -## 0 0 (B:=bool) true +## 0 0 true : 0 = 0 /\ true = true -## 0 0 (B:=bool) true +## 0 0 true : 0 = 0 /\ true = true ## 0 : 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 (B:=bool) : forall b : bool, 0 = 0 /\ b = b ## 0 0 (B:=bool) : forall b : bool, 0 = 0 /\ b = b -## 0 0 (B:=bool) true +## 0 0 true : 0 = 0 /\ true = true -## 0 0 (B:=bool) true +## 0 0 true : 0 = 0 /\ true = true diff --git a/test-suite/output/Notations5.v b/test-suite/output/Notations5.v index b3bea929ba..3c25547aac 100644 --- a/test-suite/output/Notations5.v +++ b/test-suite/output/Notations5.v @@ -181,7 +181,7 @@ Module AppliedTermsPrinting. Check v 0. (* v 0 *) Check v 0 true. - (* v 0 (B:=bool) true -- BUG *) + (* v 0 true *) Check @p nat 0. (* v *) Check @p nat 0 0. @@ -209,7 +209,7 @@ Module AppliedTermsPrinting. Check v 0. (* v 0 *) Check v 0 true. - (* v 0 (B:=bool) true -- BUG *) + (* v 0 true *) Check @p nat 0. (* v *) Check @p nat 0 0. @@ -243,9 +243,9 @@ Module AppliedTermsPrinting. Check ## 0 0. (* ## 0 0 *) Check p 0 0 true. - (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *) + (* ## 0 0 true *) Check ## 0 0 true. - (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *) + (* ## 0 0 true *) Check p 0 0 (B:=bool). (* ## 0 0 (B:=bool) *) Check ## 0 0 (B:=bool). @@ -298,16 +298,16 @@ Module AppliedTermsPrinting. (* ## 0 *) Check ## 0. (* ## 0 *) - (* Check ## 0 0. *) - (* Anomaly *) + Check ## 0 0. + (* @p nat 0 0 *) Check p 0 0 (B:=bool). (* ## 0 0 (B:=bool) *) Check ## 0 0 bool. (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *) Check p 0 0 true. - (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *) + (* ## 0 0 true *) Check ## 0 0 bool true. - (* ## 0 0 (B:=bool) true -- INCONSISTENT parsing/printing + BUG B should not be displayed *) + (* ## 0 0 true -- INCONSISTENT parsing/printing *) End NotationForPartialApplication. @@ -324,16 +324,16 @@ Module AppliedTermsPrinting. (* ## 0 *) Check ## 0. (* ## 0 *) - (* Check ## 0 0. *) - (* Anomaly *) + Check ## 0 0. + (* @p nat 0 0 *) Check p 0 0 (B:=bool). (* ## 0 0 (B:=bool) *) Check ## 0 0 bool. (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *) Check p 0 0 true. - (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *) + (* ## 0 0 true *) Check ## 0 0 bool true. - (* ## 0 0 (B:=bool) true -- INCONSISTENCY parsing/printing + BUG B should not be displayed *) + (* ## 0 0 true -- INCONSISTENCY parsing/printing *) End AtNotationForPartialApplication. |