From 043345f19f76a0a2f45a2281a57d45f6d2459e8a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 19 Nov 2006 10:39:34 +0000
Subject: 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
---
 test-suite/success/unification.v | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v
index 6886962156..7acbb7d05e 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.
-- 
cgit v1.2.3