diff options
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/1901.v')
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1901.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1901.v b/test-suite/bugs/closed/shouldsucceed/1901.v index 598db366..7d86adbf 100644 --- a/test-suite/bugs/closed/shouldsucceed/1901.v +++ b/test-suite/bugs/closed/shouldsucceed/1901.v @@ -2,9 +2,9 @@ Require Import Relations. Record Poset{A:Type}(Le : relation A) : Type := Build_Poset - { - Le_refl : forall x : A, Le x x; - Le_trans : forall x y z : A, Le x y -> Le y z -> Le x z; + { + Le_refl : forall x : A, Le x x; + Le_trans : forall x y z : A, Le x y -> Le y z -> Le x z; Le_antisym : forall x y : A, Le x y -> Le y x -> x = y }. Definition nat_Poset : Poset Peano.le. |