diff options
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/Notations2.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations2.v | 4 |
2 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index 8a18a9d855..aca872970c 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -1,2 +1,4 @@ 2 3 : PAIR +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 039771d5d5..0d5cc9e24c 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -5,3 +5,7 @@ Inductive PAIR := P (n1:nat) (n2:nat). Coercion P : nat >-> Funclass. 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. |