From 0b417c12eb10bb29bcee04384b6c0855cb9de73a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 5 Oct 2016 17:50:45 +0200
Subject: unification.ml: fix for bug #4763, unif regression

Do not force all remaining conversions problems to be solved after the
_first_ solution of an evar, but only at the end of assignment of terms
to evars in w_merge. This was hell to track down, thanks for the help of
Maxime. contribs pass and HoTT too.
---
 test-suite/bugs/closed/4763.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 test-suite/bugs/closed/4763.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4763.v b/test-suite/bugs/closed/4763.v
new file mode 100644
index 0000000000..ae8ed0e6e8
--- /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
-- 
cgit v1.2.3