1 files changed, 50 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4882.v b/test-suite/bugs/closed/4882.v
new file mode 100644
index 00000000..8c26af70
--- /dev/null
+++ b/test-suite/bugs/closed/4882.v
@@ -0,0 +1,50 @@
+
+Definition Foo {T}{a : T} : T := a.
+
+Module A.
+
+  Declare Implicit Tactic eauto.
+
+  Goal forall A (x : A), A.
+  intros.
+  apply Foo. (* Check defined evars are normalized *)
+  (*  Qed. *)
+  Abort.
+
+End A.
+
+Module B.
+
+  Definition Foo {T}{a : T} : T := a.
+
+  Declare Implicit Tactic eassumption.
+
+  Goal forall A (x : A), A.
+  intros.
+  apply Foo.
+  (*  Qed. *)
+  Abort.
+
+End B.
+
+Module C.
+
+  Declare Implicit Tactic first [exact True|assumption].
+
+  Goal forall (x : True), True.
+  intros.
+  apply (@Foo _ _).
+  Qed.
+
+End C.
+
+Module D.
+
+  Declare Implicit Tactic assumption.
+
+  Goal forall A (x : A), A.
+  intros.
+  exact _.
+  Qed.
+
+End D.