diff options
| -rw-r--r-- | test-suite/output/Intuition.v | 1 | ||||
| -rw-r--r-- | test-suite/success/Destruct.v | 4 | ||||
| -rw-r--r-- | test-suite/success/Inversion.v | 1 | ||||
| -rw-r--r-- | test-suite/success/evars.v | 9 | ||||
| -rw-r--r-- | test-suite/success/ltac.v | 22 | ||||
| -rw-r--r-- | test-suite/success/univers.v | 12 |
6 files changed, 36 insertions, 13 deletions
diff --git a/test-suite/output/Intuition.v b/test-suite/output/Intuition.v index a61735617..c0508c90b 100644 --- a/test-suite/output/Intuition.v +++ b/test-suite/output/Intuition.v @@ -2,3 +2,4 @@ Require ZArith_base. Goal (m,n:Z) `m >= n` -> `m >= m` /\ `m >= n`. Intros; Intuition. Show. +Abort. diff --git a/test-suite/success/Destruct.v b/test-suite/success/Destruct.v index 10df08728..fdd929bbc 100644 --- a/test-suite/success/Destruct.v +++ b/test-suite/success/Destruct.v @@ -7,3 +7,7 @@ Lemma foo : A->B->C. Proof. Intros. NewDestruct X. (* Should find axiom X and should handle arguments of X *) +Assumption. +Assumption. +Assumption. +Qed. diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v index 96ac86830..c28e04eb7 100644 --- a/test-suite/success/Inversion.v +++ b/test-suite/success/Inversion.v @@ -13,3 +13,4 @@ Definition Psi00 : (nat -> Prop) := [n:nat] False. Definition Psi0 : (T O) := Psi00. Lemma Inversion_RO : (l:nat)(R O Psi0 l) -> (Psi00 l). Inversion 1. +Abort. diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index f17fecc1e..a7b6d6d83 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -1,14 +1,7 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) (* The "?" of cons and eq should be inferred *) Variable list:Set -> Set. Variable cons:(T:Set) T -> (list T) -> (list T). -Goal (n:(list nat)) (EX l| (EX x| (n = (cons ? x l)))). +Check (n:(list nat)) (EX l| (EX x| (n = (cons ? x l)))). (* Examples provided by Eduardo Gimenez *) diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index bac62f16e..e93be7763 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -20,3 +20,25 @@ Tactic Definition U := Let a = 'I In Match Context With [ |- ? ] -> Apply a. Lemma lem2 : True. U. Qed. + +(* Check that Match giving non-tactic arguments are evaluated at Let-time *) + +Tactic Definition B := + Let y = (Match Context With [ z:? |- ? ] -> z) In + Intro H1; Exact y. + +Lemma lem3 : True -> False -> True -> False. +Intros H H0. +B. (* y is H0 if at let-time, H1 otherwise *) +Qed. + +(* Checks the matching order of hypotheses *) +Tactic Definition Y := Match Context With [ x:?; y:? |- ? ] -> Apply x. +Tactic Definition Z := Match Context With [ y:?; x:? |- ? ] -> Apply x. + +Lemma lem4 : (True->False) -> (False->False) -> False. +Intros H H0. +Z. (* Apply H0 *) +Y. (* Apply H *) +Exact I. +Qed. diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v index 28f9fe981..0a4b284f9 100644 --- a/test-suite/success/univers.v +++ b/test-suite/success/univers.v @@ -3,15 +3,17 @@ Definition Type2 := Type. Definition Type1 := Type : Type2. -Goal (True->Type1)->Type2. +Lemma lem1 : (True->Type1)->Type2. Intro H. Apply H. +Exact I. +Qed. -Lemma gg : (A:Type)(P:A->Type)(x:A)((y:A)(x==y)->(P y))->(P x). +Lemma lem2 : (A:Type)(P:A->Type)(x:A)((y:A)(x==y)->(P y))->(P x). Auto. Qed. -Lemma titi : (P:Prop)P. +Lemma lem3 : (P:Prop)P. Intro P ; Pattern P. -Apply gg. - +Apply lem2. +Abort. |