1 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1901.v b/test-suite/bugs/closed/shouldsucceed/1901.v
new file mode 100644
index 00000000..598db366
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1901.v
@@ -0,0 +1,11 @@
+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_antisym : forall x y : A, Le x y -> Le y x -> x = y }.
+
+Definition nat_Poset : Poset Peano.le.
+Admitted.
+\ No newline at end of file