diff options
| -rw-r--r-- | tests/matching.v | 19 | ||||
| -rw-r--r-- | theories/Pattern.v | 2 |
2 files changed, 20 insertions, 1 deletions
diff --git a/tests/matching.v b/tests/matching.v index 6bc5706da7..4338cbd32f 100644 --- a/tests/matching.v +++ b/tests/matching.v @@ -50,3 +50,22 @@ match! reverse goal with check_id h' @i end. Abort. + +(* Check #79 *) +Goal 2 = 3. + Control.plus + (fun () + => lazy_match! goal with + | [ |- 2 = 3 ] => Control.zero (Tactic_failure None) + | [ |- 2 = _ ] => Control.zero (Tactic_failure (Some (Message.of_string "should not be printed"))) + end) + (fun e + => match e with + | Tactic_failure c + => match c with + | None => () + | _ => Control.zero e + end + | e => Control.zero e + end). +Abort. diff --git a/theories/Pattern.v b/theories/Pattern.v index ff7776b682..8d1fb0cd8a 100644 --- a/theories/Pattern.v +++ b/theories/Pattern.v @@ -125,7 +125,7 @@ Ltac2 lazy_goal_match0 rev pats := in Control.plus cur next end in - interp pats (). + Control.once (fun () => interp pats) (). Ltac2 multi_goal_match0 rev pats := let rec interp m := match m with |