From 49155a0817234299c45d04a14bd834f44fbc391f Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Mon, 28 Jan 2019 18:00:02 -0500
Subject: Make lazy_match! goal actually lazy

It was missing `Control.once`.

Fixes coq/ltac2#79
Fixes coq/ltac2#77
---
 theories/Pattern.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories/Pattern.v')

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
-- 
cgit v1.2.3