diff options
| author | herbelin | 2011-11-06 15:55:57 +0000 |
|---|---|---|
| committer | herbelin | 2011-11-06 15:55:57 +0000 |
| commit | 88789202027f7d8e6a2bc6ec4493dd44d512fb64 (patch) | |
| tree | 8f91c02ec5f3dc83d0f13a76cedd4ebbcc778eaf /test-suite | |
| parent | d9b82a2d4a9e310f9f0cd907e71bc6a57bf03efd (diff) | |
Fixing incorrect change to pattern-unification over Meta's introduced
in r14199 (June 2011). Meta's implicitly depend on the context they are
defined in and this has to be taken into account for checking if
occurrences are distinct (in particular, no Var's are allowed as
arguments of a pattern-unifiable Meta). The example expected to be
accepted thanks to r14199 is not a pattern-unification problem (it has
more than one solution) and was anyway already accepted (strange).
Compared to before r14199, aliases expansion and restriction of
pattern unification check to variables occurring in the right-hand
side are however now taken into account.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14642 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/rewrite.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v index 3d49d3cf93..08c406be94 100644 --- a/test-suite/success/rewrite.v +++ b/test-suite/success/rewrite.v @@ -118,4 +118,14 @@ Axiom s : forall (A B : Type) (p : A * B), p = (fst p, snd p). Definition P := (nat * nat)%type. Goal forall x:P, x = x. intros. rewrite s. +Abort. + +(* Test second-order unification and failure of pattern-unification *) + +Goal forall (P: forall Y, Y -> Prop) Y a, Y = nat -> (True -> P Y a) -> False. +intros. +(* The next line used to succeed between June and November 2011 *) +(* causing ill-typed rewriting *) +Fail rewrite H in H0. +Abort. |