Provide a reinit data for Ltac2 notations with entry level 4.

The grammar engine has the great idea to silently delete empty levels on rule
removal. Since Ltac2 level 4 is initially empty, it means that when backtracking
on the loading of the Ltac2 plugin, the grammar would be in a state where the
level 4 was not there at all.

There is a dedicated API for that situation in Pcoq, but it is kind of crazy
that we have to use this kind of workaround when the problem is clearly that
gramlib has the wrong default.

Fixes #14156: Ltac2 broken with async.

1 files changed, 18 insertions, 9 deletions

diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index 6aa31e9c91..7d17bd3d33 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -631,7 +631,7 @@ let parse_scope = ParseToken.parse_scope
 type synext = {
   synext_tok : sexpr list;
   synext_exp : raw_tacexpr;
-  synext_lev : int option;
+  synext_lev : int;
   synext_loc : bool;
   synext_depr : Deprecation.t option;
 }
@@ -660,6 +660,14 @@ let deprecated_ltac2_notation =
     ~warning_name:"deprecated-ltac2-notation"
     (fun (toks : sexpr list) -> pr_sequence ParseToken.print_token toks)
 
+(* This is a hack to preserve the level 4 entry which is initially empty. The
+   grammar engine has the great idea to silently delete empty levels on rule
+   removal, so we have to work around this using the Pcoq API.
+   FIXME: we should really keep those levels around instead. *)
+let get_reinit = function
+| 4 -> Some (Gramlib.Gramext.LeftA, Gramlib.Gramext.After "5")
+| _ -> None
+
 let perform_notation syn st =
   let tok = List.rev_map ParseToken.parse_token syn.synext_tok in
   let KRule (rule, act) = get_rule tok in
@@ -675,12 +683,13 @@ let perform_notation syn st =
     CAst.make ~loc @@ CTacLet (false, bnd, syn.synext_exp)
   in
   let rule = Pcoq.Production.make rule (act mk) in
-  let pos = match syn.synext_lev with
-  | None -> None
-  | Some lev -> Some (Gramlib.Gramext.Level (string_of_int lev))
-  in
-  let rule = (None, None, [rule]) in
-  ([Pcoq.ExtendRule (Pltac.ltac2_expr, {Pcoq.pos; data=[rule]})], st)
+  let pos = Some (Gramlib.Gramext.Level (string_of_int syn.synext_lev)) in
+  let rule = {Pcoq.pos; data = [(None, None, [rule])] } in
+  match get_reinit syn.synext_lev with
+  | None ->
+    ([Pcoq.ExtendRule (Pltac.ltac2_expr, rule)], st)
+  | Some reinit ->
+    ([Pcoq.ExtendRuleReinit (Pltac.ltac2_expr, reinit, rule)], st)
 
 let ltac2_notation =
   Pcoq.create_grammar_command "ltac2-notation" perform_notation
@@ -760,8 +769,8 @@ let register_notation ?deprecation ?(local = false) tkn lev body = match tkn, le
       if n < 0 || n > 6 then
         user_err (str "Notation levels must range between 0 and 6")
     in
-    lev
-  | None -> Some 5
+    n
+  | None -> 5
   in
   let ext = {
     synext_tok = tkn;