3 files changed, 42 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5219.v b/test-suite/bugs/closed/5219.v
new file mode 100644
index 0000000000..f7cec1a0cf
--- /dev/null
+++ b/test-suite/bugs/closed/5219.v
@@ -0,0 +1,10 @@
+(* Test surgical use of beta-iota in the type of variables coming from
+   pattern-matching for refine *)
+
+Goal forall x : sigT (fun x => x = 1), True.
+  intro x; refine match x with
+                  | existT _ x' e' => _
+                  end.
+  lazymatch goal with
+  | [ H : _ = _ |- _ ] => idtac
+  end.
diff --git a/test-suite/success/transparent_abstract.v b/test-suite/success/transparent_abstract.v
new file mode 100644
index 0000000000..ff4509c4a8
--- /dev/null
+++ b/test-suite/success/transparent_abstract.v
@@ -0,0 +1,21 @@
+Class by_transparent_abstract {T} (x : T) := make_by_transparent_abstract : T.
+Hint Extern 0 (@by_transparent_abstract ?T ?x) => change T; transparent_abstract exact_no_check x : typeclass_instances.
+
+Goal True /\ True.
+Proof.
+  split.
+  transparent_abstract exact I using foo.
+  let x := (eval hnf in foo) in constr_eq x I.
+  let x := constr:(ltac:(constructor) : True) in
+  let T := type of x in
+  let x := constr:(_ : by_transparent_abstract x) in
+  let x := (eval cbv delta [by_transparent_abstract] in (let y : T := x in y)) in
+  pose x as x'.
+  simpl in x'.
+  let v := eval cbv [x'] in x' in tryif constr_eq v I then fail 0 else idtac.
+  hnf in x'.
+  let v := eval cbv [x'] in x' in tryif constr_eq v I then idtac else fail 0.
+  exact x'.
+Defined.
+Check eq_refl : I = foo.
+Eval compute in foo.
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" *)