From ab8e47207245277cb5b92b80a92ae78ede5bfafe Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Tue, 12 Dec 2017 15:32:59 +0000
Subject: [vernac] vernac_expr no longer recursive

---
 stm/proofBlockDelimiter.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'stm/proofBlockDelimiter.ml')

diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 01b5b9a016..bebc4d5d5f 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -96,7 +96,7 @@ let dynamic_bullet doc { dynamic_switch = id; carry_on_data = b } =
       `ValidBlock {
          base_state = id;
          goals_to_admit = focused;
-         recovery_command = Some (Vernacexpr.VernacExpr(Vernacexpr.VernacBullet (to_bullet_val b)))
+         recovery_command = Some (Vernacexpr.VernacExpr([], Vernacexpr.VernacBullet (to_bullet_val b)))
       }
   | `Not -> `Leaks
 
@@ -125,7 +125,7 @@ let dynamic_curly_brace doc { dynamic_switch = id } =
       `ValidBlock {
          base_state = id;
          goals_to_admit = focused;
-         recovery_command = Some (Vernacexpr.VernacExpr Vernacexpr.VernacEndSubproof)
+         recovery_command = Some (Vernacexpr.VernacExpr ([], Vernacexpr.VernacEndSubproof))
       }
   | `Not -> `Leaks
 
-- 
cgit v1.2.3