diff options
Diffstat (limited to 'test-suite/output/ltac.v')
| -rw-r--r-- | test-suite/output/ltac.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v index 6adbe95d..901b1e3a 100644 --- a/test-suite/output/ltac.v +++ b/test-suite/output/ltac.v @@ -37,17 +37,20 @@ Fail g1 I. Fail f1 I. Fail g2 I. Fail f2 I. +Abort. Ltac h x := injection x. Goal True -> False. Fail h I. intro H. Fail h H. +Abort. (* 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. +Abort. (* Check consistency of interpretation scopes (#4398) *) |