From 84aaa74ff9537dfdfc214ab60f8acf42466878b1 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 17 Sep 2010 16:02:50 +0000
Subject: 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
---
 test-suite/success/auto.v | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 test-suite/success/auto.v

(limited to 'test-suite')

diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v
new file mode 100644
index 0000000000..a2701f8bbe
--- /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.
-- 
cgit v1.2.3