diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index c29be6173cada..ecd2786ef5624 100644 --- 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