Make lazy_match! goal actually lazy

It was missing `Control.once`.

Fixes coq/ltac2#79
Fixes coq/ltac2#77

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