Raffinement de l'unification de "apply": mémorisation de certains

degrés de liberté concernant les instances de méta (cumulativité et
possibilité d'éta-expansion) de telle sorte que la fusion d'équations
se fasse modulo ces degrés de liberté.


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

1 files changed, 20 insertions, 0 deletions

diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v
index 688696215..7acbb7d05 100644
--- a/test-suite/success/unification.v
+++ b/test-suite/success/unification.v
@@ -63,3 +63,23 @@ Proof.
 intros.
 apply H.
 Qed.
+
+
+(* Test unification modulo eta-expansion (if possible) *)
+
+(* In this example, two instances for ?P (argument of hypothesis H) can be 
+   inferred (one is by unifying the type [Q true] and [?P true] of the
+   goal and type of [H]; the other is by unifying the argument of [f]);
+   we need to unify both instances up to allowed eta-expansions of the 
+   instances (eta is allowed if the meta was applied to arguments)
+
+   This used to fail before revision 9389 in trunk
+*)
+
+Lemma l4 :
+   forall f : (forall P, P true), (forall P, f P = f P) ->
+   forall Q, f (fun x => Q x) = f (fun x => Q x).
+Proof.
+intros.
+apply H.
+Qed.