In the computation of missing arguments for apply, accept that the

user either gives all missing arguments not dependent in the concl or
all missing arguments not *recursively* dependent in the concl (as
introduced by commit 13367). In practice, this means that "apply
f_equal with A" remains allowed even though the new, recursive,
analysis detects that all arguments of f_equal are inferable,
including the first type argument (which is inferable from the
knowledge of the function).
Sized the opportunity to better explain the behavior of clenv_dependent.
Also made minor code simplification.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13426 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 18 insertions, 0 deletions

diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v
new file mode 100644
index 000000000..a2701f8bb
--- /dev/null
+++ b/test-suite/success/auto.v
@@ -0,0 +1,18 @@
+(* Wish #2154 by E. van der Weegen *)
+
+(* auto was not using f_equal-style lemmas with metavariables occuring
+   only in the type of an evar of the concl, but not directly in the
+   concl itself *)
+
+Parameters
+  (F: Prop -> Prop)
+  (G: forall T, (T -> Prop) -> Type)
+  (L: forall A (P: A -> Prop), G A P -> forall x, F (P x))
+  (Q: unit -> Prop).
+
+Hint Resolve L.
+
+Goal G unit Q -> F (Q tt).
+  intro.
+  auto.
+Qed.