From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- test-suite/output/ltac.v | 42 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 42 insertions(+) (limited to 'test-suite/output/ltac.v') diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v index 7e2610c7..76c37625 100644 --- a/test-suite/output/ltac.v +++ b/test-suite/output/ltac.v @@ -15,3 +15,45 @@ lazymatch goal with | H1 : HT |- _ => idtac end. Abort. + +Ltac f x y z := + symmetry in x, y; + auto with z; + auto; + intros; + clearbody x; + generalize dependent z. + +Print Ltac f. + +(* Error messages *) + +Ltac g1 x := refine x. +Tactic Notation "g2" constr(x) := g1 x. +Tactic Notation "f1" constr(x) := refine x. +Ltac f2 x := f1 x. +Goal False. +Fail g1 I. +Fail f1 I. +Fail g2 I. +Fail f2 I. + +Ltac h x := injection x. +Goal True -> False. +Fail h I. +intro H. +Fail h H. + +(* Check printing of the "var" argument "Hx" *) +Ltac m H := idtac H; exact H. +Goal True. +let a:=constr:(let Hx := 0 in ltac:(m Hx)) in idtac. + +(* Check consistency of interpretation scopes (#4398) *) + +Goal nat*(0*0=0) -> nat*(0*0=0). intro. +match goal with H: ?x*?y |- _ => idtac x end. +match goal with |- ?x*?y => idtac x end. +match goal with H: context [?x*?y] |- _ => idtac x end. +match goal with |- context [?x*?y] => idtac x end. +Abort. -- cgit v1.2.3