From dae240f31d6de1d5b3737d6d0779e009f3d67fa2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Fri, 1 Jul 2016 12:48:26 +0200
Subject: Fixing #4882 (anomaly with Declare Implicit Tactic on hole of type
 with evars).

But there are still bugs with Declare Implicit Tactic, which should
probably rather be reimplemented with ltac:(tac).

Indeed, it does support evars in the type of the term, and
solve_by_implicit_tactic should transfer universe constraints to the
main goal. E.g., the following still fails, at Qed time.

Definition Foo {T}{a : T} : T := a.
Declare Implicit Tactic eassumption.
Goal forall A (x : A), A.
intros.
apply Foo.
Qed.
---
 test-suite/bugs/closed/4882.v | 50 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 50 insertions(+)
 create mode 100644 test-suite/bugs/closed/4882.v

(limited to 'test-suite/bugs/closed/4882.v')

diff --git a/test-suite/bugs/closed/4882.v b/test-suite/bugs/closed/4882.v
new file mode 100644
index 000000000..8c26af708
--- /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.
-- 
cgit v1.2.3