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.

0 files changed, 0 insertions, 0 deletions