diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Notations2.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations2.v | 9 |
2 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index aca872970c..c1a7e961a9 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -1,4 +1,6 @@ 2 3 : PAIR +2[+]3 + : nat forall (A : Set) (le : A -> A -> Prop) (x y : A), le x y \/ le y x : Prop diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index 0d5cc9e24c..3eeff401cf 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -6,6 +6,15 @@ Inductive PAIR := P (n1:nat) (n2:nat). Coercion P : nat >-> Funclass. Check (2 3). +(* Check that notations with coercions to functions inserted still work *) +(* (were not working from revision 11886 to 12951) *) + +Record Binop := { binop :> nat -> nat -> nat }. +Class Plusop := { plusop : Binop; z : nat }. +Infix "[+]" := plusop (at level 40). +Instance Plus : Plusop := {| plusop := {| binop := plus |} ; z := 0 |}. +Check 2[+]3. + (* Test bug #2091 (variable le was printed using <= !) *) Check forall (A: Set) (le: A -> A -> Prop) (x y: A), le x y \/ le y x. |