diff options
Diffstat (limited to 'test-suite/success/ltac.v')
-rw-r--r-- | test-suite/success/ltac.v | 33 |
1 files changed, 28 insertions, 5 deletions
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 757cf6a4..dfa41c82 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -3,7 +3,7 @@ (* Submitted by Pierre Crégut *) (* Checks substitution of x *) Ltac f x := unfold x in |- *; idtac. - + Lemma lem1 : 0 + 0 = 0. f plus. reflexivity. @@ -25,7 +25,7 @@ U. Qed. (* Check that Match giving non-tactic arguments are evaluated at Let-time *) - + Ltac B := let y := (match goal with | z:_ |- _ => z end) in @@ -152,6 +152,7 @@ Abort. Ltac afi tac := intros; tac. Goal 1 = 2. afi ltac:auto. +Abort. (* Tactic Notation avec listes *) @@ -179,8 +180,8 @@ Abort. (* Check second-order pattern unification *) Ltac to_exist := - match goal with - |- forall x y, @?P x y => + 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. @@ -201,7 +202,7 @@ Abort. (* Utilisation de let rec sans arguments *) -Ltac is := +Ltac is := let rec i := match goal with |- ?A -> ?B => intro; i | _ => idtac end in i. @@ -220,3 +221,25 @@ Z1 O. Z2 ltac:O. exact I. Qed. + +(* Illegal application used to make Ltac loop. *) + +Section LtacLoopTest. + Ltac f x := idtac. + Goal True. + Timeout 1 try f()(). + Abort. +End LtacLoopTest. + +(* Test binding of open terms *) + +Ltac test_open_match z := + match z with + (forall y x, ?h = 0) => assert (forall x y, h = x + y) + end. + +Goal True. +test_open_match (forall z y, y + z = 0). +reflexivity. +apply I. +Qed. |