3 files changed, 30 insertions, 10 deletions
diff --git a/user-contrib/Ltac2/Bool.v b/user-contrib/Ltac2/Bool.v
index 624097728e..b201574808 100644
--- a/user-contrib/Ltac2/Bool.v
+++ b/user-contrib/Ltac2/Bool.v
@@ -48,7 +48,7 @@ Ltac2 xor x y :=
        end
   end.
 
-Ltac2 eq x y :=
+Ltac2 equal x y :=
   match x with
   | true
     => match y with
@@ -61,3 +61,6 @@ Ltac2 eq x y :=
        | false => true
        end
   end.
+
+#[deprecated(note="Use Bool.equal", since="8.14")]
+Ltac2 eq := equal.
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index 7af530ab0f..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 lev = match syn.synext_lev with
-  | None -> None
-  | Some lev -> Some (string_of_int lev)
-  in
-  let rule = (lev, None, [rule]) in
-  ([Pcoq.ExtendRule (Pltac.ltac2_expr, {Pcoq.pos=None; 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
@@ -754,7 +763,15 @@ let register_notation ?deprecation ?(local = false) tkn lev body = match tkn, le
   let ids = List.fold_left fold Id.Set.empty entries in
   (* Globalize so that names are absolute *)
   let body = Tac2intern.globalize ids body in
-  let lev = match lev with Some _ -> lev | None -> Some 5 in
+  let lev = match lev with
+  | Some n ->
+    let () =
+      if n < 0 || n > 6 then
+        user_err (str "Notation levels must range between 0 and 6")
+    in
+    n
+  | None -> 5
+  in
   let ext = {
     synext_tok = tkn;
     synext_exp = body;
diff --git a/user-contrib/Ltac2/tac2intern.ml b/user-contrib/Ltac2/tac2intern.ml
index 206f4df19d..0171ddfcf8 100644
--- a/user-contrib/Ltac2/tac2intern.ml
+++ b/user-contrib/Ltac2/tac2intern.ml
@@ -468,7 +468,7 @@ let polymorphic ((n, t) : type_scheme) : mix_type_scheme =
 let warn_not_unit =
   CWarnings.create ~name:"not-unit" ~category:"ltac"
     (fun (env, t) ->
-      strbrk "The following expression should have type unit but has type " ++
+      strbrk "This expression should have type unit but has type " ++
       pr_glbtype env t ++ str ".")
 
 let warn_redundant_clause =