[ssr] Stop relying on camlp5 recovery mechanism

for "do [tac] => intro" and "tac; [tac|..|tac] => intro"
coq · Oct 30, 2023 · 6db7a0f · 6db7a0f
1 parent 7861b99
commit 6db7a0f
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
@@ -1717,7 +1717,10 @@ let tclintros_expr ?loc tac ipats =
 
 GRAMMAR EXTEND Gram
   GLOBAL: ltac_expr;
-  ltac_expr: LEVEL "1" [
+  ltac_expr: LEVEL "3" [
+    [ tac = ltac_expr; intros = ssrintros_ne -> { tclintros_expr ~loc tac intros }
+    ] ];
+  ltac_expr: LEVEL "4" [
     [ tac = ltac_expr; intros = ssrintros_ne -> { tclintros_expr ~loc tac intros }
     ] ];
 END