diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-02-13 18:47:49 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-02-13 18:47:49 +0000 |
commit | 34ba48a885c91ea895cbba7ba5a53b1ec9de5db8 (patch) | |
tree | 7c793d76af431bc2cb0aa78e7e9edaa991d1892f /test-suite/success/ltac.v | |
parent | 6e9c0edd9efc9d72e6f32bc434a34076b1a6afee (diff) |
Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de
fonctionner entre la V7.3 et la V8.0 (notation : "@ ?meta id1 ... idn")
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9644 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/ltac.v')
-rw-r--r-- | test-suite/success/ltac.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 3f25f7035..05a6a70f3 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -175,3 +175,16 @@ Abort. Goal True. match None with @None => exact I end. Abort. + +(* Check second-order pattern unification *) + +Ltac to_exist := + match goal with + |- forall x y, @?P x y => + let Q := eval lazy beta in (exists x, forall y, P x y) in + assert (Q->Q) + end. + +Goal forall x y : nat, x = y. +to_exist. exact (fun H => H). +Abort. |