Imported Upstream version 8.5~beta1+dfsg

1 files changed, 13 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/1891.v b/test-suite/bugs/closed/1891.v
new file mode 100644
index 00000000..68581117
--- /dev/null
+++ b/test-suite/bugs/closed/1891.v
@@ -0,0 +1,13 @@
+(* Check evar-evar unification *)
+ Inductive T (A: Set): Set := mkT: unit -> T A.
+
+  Definition f (A: Set) (l: T A): unit := tt.
+
+  Implicit Arguments f [A].
+
+  Lemma L (x: T unit): (unit -> T unit) -> unit.
+  Proof.
+    refine (match x return _ with mkT _ n => fun g => f (g _) end).
+    trivial.
+  Qed.
+