summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/1891.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/closed/1891.v')
-rw-r--r--test-suite/bugs/closed/1891.v13
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.
+