From cff6f53cbef53ce3902e59853f7a7dc9b7150f45 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 1 May 2017 13:25:10 +0200
Subject: Adding a test-suite pattern-unification example that Econstr fixed.

---
 test-suite/success/unification.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v
index 296686e16e..6f7498d659 100644
--- a/test-suite/success/unification.v
+++ b/test-suite/success/unification.v
@@ -188,3 +188,14 @@ Proof.
   apply idpath.
   apply idpath.
 Defined.
+
+(* An example where it is necessary to evar-normalize the instance of
+   an evar to evaluate if it is a pattern *)
+
+Check
+  let a := ?[P] in
+  fun (H : forall y (P : nat -> Prop), y = 0 -> P y)
+      x (p:x=0) =>
+    H ?[y] a p : x = 0.
+(* We have to solve "?P ?y[x] == x = 0" knowing from
+   "p : (x=0) == (?y[x] = 0)" that "?y := x" *)
-- 
cgit v1.2.3