From dae240f31d6de1d5b3737d6d0779e009f3d67fa2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
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.
---
 proofs/pfedit.ml              |  4 +++-
 test-suite/bugs/closed/4882.v | 50 +++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 53 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/4882.v

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index a515c9e750..20cae84a49 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -230,8 +230,10 @@ let solve_by_implicit_tactic env sigma evk =
 	(Environ.named_context env) ->
       let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) []) in
       (try
+        let c = Evarutil.nf_evars_universes sigma evi.evar_concl in
+        if Evarutil.has_undefined_evars sigma c then raise Exit;
         let (ans, _, _) = 
-	  build_by_tactic env (Evd.evar_universe_context sigma) evi.evar_concl tac in
+	  build_by_tactic env (Evd.evar_universe_context sigma) c tac in
         ans
        with e when Logic.catchable_exception e -> raise Exit)
   | _ -> raise Exit
diff --git a/test-suite/bugs/closed/4882.v b/test-suite/bugs/closed/4882.v
new file mode 100644
index 0000000000..8c26af708b
--- /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