1 files changed, 13 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4763.v b/test-suite/bugs/closed/4763.v
new file mode 100644
index 00000000..ae8ed0e6
--- /dev/null
+++ b/test-suite/bugs/closed/4763.v
@@ -0,0 +1,13 @@
+Require Import Coq.Arith.Arith Coq.Classes.Morphisms Coq.Classes.RelationClasses.
+Coercion is_true : bool >-> Sortclass.
+Global Instance: Transitive leb.
+Admitted.
+
+Goal forall x y z, leb x y -> leb y z -> True.
+  intros ??? H H'.
+  lazymatch goal with
+  | [ H : is_true (?R ?x ?y), H' : is_true (?R ?y ?z) |- _ ]
+    => pose proof (transitivity H H' : is_true (R x z))
+  end.
+  exact I.
+Qed.
+\ No newline at end of file