diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index b465dfc175e8..8cac34624aab 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -635,7 +635,7 @@ library:ci-bbv:
   - build:base
   - library:ci-stdlib
 
-library:ci-bedrock2:
+.library:ci-bedrock2:
   extends: .ci-template-flambda
   variables:
     NJOBS: "1"
@@ -648,7 +648,7 @@ library:ci-bedrock2:
   - library:ci-riscv_coq
   stage: build-3+
 
-library:ci-bedrock2_examples:
+.library:ci-bedrock2_examples:
   extends: .ci-template-flambda
   variables:
     NJOBS: "1"
@@ -752,7 +752,7 @@ library:ci-fcsl_pcm:
   - library:ci-mathcomp
   stage: build-2
 
-library:ci-fiat_crypto:
+.library:ci-fiat_crypto:
   extends: .ci-template-flambda
   variables:
     COQEXTRAFLAGS: "-async-proofs-tac-j 0"
@@ -780,7 +780,7 @@ library:ci-fiat_crypto_legacy:
 # We cannot use flambda due to
 # https://github.com/ocaml/ocaml/issues/7842, see
 # https://github.com/rocq-prover/rocq/pull/11916#issuecomment-609977375
-library:ci-fiat_crypto_ocaml:
+.library:ci-fiat_crypto_ocaml:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
@@ -803,7 +803,7 @@ library:ci-flocq:
   - build:edge+flambda
   - library:ci-stdlib+flambda
 
-library:ci-kami:
+.library:ci-kami:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
@@ -976,7 +976,7 @@ library:ci-simple_io:
   - library:ci-ext_lib
   stage: build-2
 
-library:ci-sf:
+.library:ci-sf:  # disabled until https://github.com/DeepSpec/sf/pull/16 can get in / the process for overlays there can be documented
   extends: .ci-template
   needs:
   - build:base
@@ -1287,7 +1287,7 @@ library:ci-riscv_coq:
   - library:ci-coqutil
   stage: build-2
 
-library:ci-rupicola:
+.library:ci-rupicola:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
diff --git a/doc/changelog/11-corelib/17876-master+gramlib-support-for-non-assoc-and-non-recovery-Changed.rst b/doc/changelog/11-corelib/17876-master+gramlib-support-for-non-assoc-and-non-recovery-Changed.rst
new file mode 100644
index 000000000000..51563b47f05a
--- /dev/null
+++ b/doc/changelog/11-corelib/17876-master+gramlib-support-for-non-assoc-and-non-recovery-Changed.rst
@@ -0,0 +1,5 @@
+- **Changed:**
+  Level of ``_~0`` and ``_~1`` reserved notations (used for positive
+  numbers) from level 7 to level 1
+  (`#17876 <https://github.com/rocq-prover/rocq/pull/17876>`_,
+  by Pierre Roux).
diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst
index 9ae6bf91c1cd..ac2d78a0eef2 100644
--- a/doc/sphinx/language/extensions/canonical.rst
+++ b/doc/sphinx/language/extensions/canonical.rst
@@ -538,10 +538,10 @@ We need some infrastructure for that.
     Definition id {T} {t : T} (x : phantom t) := x.
 
     Notation "[find v | t1 ~ t2 ] p" := (fun v (_ : unify t1 t2 None) => p)
-      (at level 50, v name, only parsing).
+      (at level 50, v name, p at level 50, only parsing).
 
     Notation "[find v | t1 ~ t2 | s ] p" := (fun v (_ : unify t1 t2 (Some s)) => p)
-      (at level 50, v name, only parsing).
+      (at level 50, v name, p at level 50, only parsing).
 
     Notation "'Error : t : s" := (unify _ t (Some s))
       (at level 50, format "''Error' : t : s").
diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index dfb884f27cbb..9ab066028a94 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -140,6 +140,8 @@ module type ExtS = sig
     type t = {
       estate : EState.t;
       kwstate : keyword_state;
+      recover : bool;
+      has_non_assoc : bool;
     }
   end
 
@@ -192,19 +194,6 @@ type 'a ty_entry = {
   etag : 'a DMap.onetag;
 }
 
-and 'a ty_desc =
-| Dlevels of 'a ty_level list
-| Dparser of (L.keyword_state -> 'a parser_t)
-
-and 'a ty_level = Level : (_, _, 'a) ty_rec_level -> 'a ty_level
-
-and ('trecs, 'trecp, 'a) ty_rec_level = {
-  assoc : g_assoc;
-  lname : string option;
-  lsuffix : ('a, 'trecs, 'a -> Loc.t -> 'a) ty_tree;
-  lprefix : ('a, 'trecp, Loc.t -> 'a) ty_tree;
-}
-
 and ('self, 'trec, 'a) ty_symbol =
 | Stoken : 'c pattern -> ('self, norec, 'c) ty_symbol
 | Stokens : ty_pattern list -> ('self, norec, unit) ty_symbol
@@ -235,6 +224,19 @@ and ('self, 'trec, 'trecs, 'trecb, 'a, 'r) ty_node = {
   brother : ('self, 'trecb, 'r) ty_tree;
 }
 
+type ('trecs, 'trecp, 'a) ty_rec_level = {
+  assoc : g_assoc;
+  lname : string option;
+  lsuffix : ('a, 'trecs, 'a -> Loc.t -> 'a) ty_tree;
+  lprefix : ('a, 'trecp, Loc.t -> 'a) ty_tree;
+}
+
+type 'a ty_level = Level : (_, _, 'a) ty_rec_level -> 'a ty_level
+
+type 'a ty_desc =
+| Dlevels of 'a ty_level list
+| Dparser of (L.keyword_state -> 'a parser_t)
+
 (** The closures are built by partially applying the parsing functions
     to [edesc] but without depending on the state (so when we update
     an entry we don't need to update closures in unrelated entries).
@@ -246,7 +248,7 @@ type ('t,'a) entry_data = {
   eentry : 'a ty_entry;
   edesc : 'a ty_desc;
   estart : 't -> int -> 'a parser_t;
-  econtinue : 't -> int -> int -> 'a -> 'a parser_t;
+  econtinue : 't -> int option -> int -> int -> 'a -> 'a parser_t;
 }
 
 module rec EState : DMap.MapS
@@ -257,11 +259,15 @@ and GState : sig
   type t = {
     estate : EState.t;
     kwstate : L.keyword_state;
+    recover : bool;
+    has_non_assoc : bool;
   }
 end = struct
   type t = {
     estate : EState.t;
     kwstate : L.keyword_state;
+    recover : bool;
+    has_non_assoc : bool;
   }
 end
 open GState
@@ -1021,14 +1027,53 @@ let top_tree : type s tr a. s ty_entry -> (s, tr, a) ty_tree -> (s, tr, a) ty_tr
       Node (NoRec3, {node = top_symb entry s; brother = bro; son = son})
   | LocAct (_, _) -> raise Stream.Failure | DeadEnd -> raise Stream.Failure
 
+let warn_tolerance =
+  CWarnings.(create_in (create_warning ~name:"level-tolerance"
+                          ~from:[CoreCategories.parsing; Deprecation.Version.v9_2] ())
+    Pp.(fun (cur_lev,top_lev) ->
+        let f = function None -> "<unknown>" | Some s -> s in
+        strbrk "Tolerating this expression at level " ++ str (f cur_lev) ++
+        strbrk " while it is expected to be at level " ++ str (f top_lev) ++ str "." ++
+        strbrk " This tolerance will be eventually removed." ++
+        strbrk " Insert parentheses or try to lower the level at which the top symbol of this expression is parsed."))
+
+type capsule = Capsule : 's ty_entry * ('s, 't, 'a) ty_symbol -> capsule
+
+let get_node : type s tr a. s ty_entry -> (s, tr, a) ty_tree -> capsule
+  = fun entry -> function
+    | Node (MayRec3, {node = s; brother = bro; son = son}) -> Capsule (entry, s)
+    | Node (NoRec3, {node = s; brother = bro; son = son}) -> Capsule (entry, s)
+    | _ -> assert false
+
+let warn_recover nlevn alevn (Capsule (entry, s)) gstate bp strm__ =
+  let ep = LStream.count strm__ in
+  let loc = LStream.interval_loc bp ep strm__ in
+  try
+    let find_lev levn = function
+      | Dlevels levs -> let Level levs = List.nth levs levn in levs.lname
+      | _ -> raise Exit in
+    let rec find_symb : type s tr a. s ty_entry -> (s, tr, a) ty_symbol -> _ = fun entry -> function
+      | Sself -> let levs = (get_entry gstate.estate entry).edesc in find_lev alevn levs, find_lev 0 levs
+      | Snext -> let levs = (get_entry gstate.estate entry).edesc in find_lev nlevn levs, find_lev 0 levs
+      | Snterml (e, levn) -> Some levn, find_lev 0 (get_entry gstate.estate e).edesc
+      | Slist1sep (s, sep, b) -> find_symb entry s
+      | _ -> assert false in
+    let cur_lev, top_lev = try find_symb entry s with Failure _ -> None, None in
+    warn_tolerance ~loc (cur_lev,top_lev)
+  with Exit -> ()
+
+let warn_recover_continuation bp ep strm__ =
+  let loc = LStream.interval_loc bp ep strm__ in
+  warn_tolerance ~loc (None, None)
+
 let empty_entry ename levn strm =
   raise (Error ("entry [" ^ ename ^ "] is empty"))
 
 let start_parser_of_entry gstate entry levn (strm:_ LStream.t) =
   (get_entry gstate.estate entry).estart gstate levn strm
 
-let continue_parser_of_entry gstate entry levn bp a (strm:_ LStream.t) =
-  (get_entry gstate.estate entry).econtinue gstate levn bp a strm
+let continue_parser_of_entry gstate entry levfrom levn bp a (strm:_ LStream.t) =
+  (get_entry gstate.estate entry).econtinue gstate levfrom levn bp a strm
 
 (**
   nlevn: level for Snext
@@ -1095,6 +1140,13 @@ and parser_cont : type s tr tr' a r.
     Stream.Failure ->
     (* Recover from a success on [s] with result [a] followed by a
         failure on [son] in a rule of the form [a = s; son] *)
+    (* Discard the rule if what has been consumed before failing is
+       the empty sequence (due to some OPT or LIST0); example:
+       « OPT "!"; ident » fails to see an ident and the OPT was resolved
+       into the empty sequence, with application e.g. to being able to
+       safely write « LIST1 [ OPT "!"; id = ident -> id] ». *)
+    if LStream.count strm__ == bp then fun a -> raise Stream.Failure
+    else
     try
       (* Try to replay the son with the top occurrence of NEXT (by
          default at level nlevn) and trailing SELF (by default at alevn)
@@ -1104,16 +1156,14 @@ and parser_cont : type s tr tr' a r.
          « SELF; "\/"; same-entry-at-top-level » with application e.g. to
          accept "A \/ forall x, x = x" w/o requiring the expected
          parentheses as in "A \/ (forall x, x = x)". *)
-      parser_of_tree entry nlevn alevn (top_tree entry son) gstate strm__
+      if gstate.recover then
+        let a = parser_of_tree entry nlevn alevn (top_tree entry son) gstate strm__ in
+        warn_recover nlevn alevn (get_node entry son) gstate bp strm__;
+        a
+      else
+        raise Stream.Failure
     with
       Stream.Failure ->
-      (* Discard the rule if what has been consumed before failing is
-         the empty sequence (due to some OPT or LIST0); example:
-         « OPT "!"; ident » fails to see an ident and the OPT was resolved
-         into the empty sequence, with application e.g. to being able to
-         safely write « LIST1 [ OPT "!"; id = ident -> id] ». *)
-      if LStream.count strm__ == bp then fun a -> raise Stream.Failure
-      else
         (* In case of success on just SELF, NEXT or an explicit call to
            a subentry followed by a failure on the rest (son), retry
            parsing as if this entry had been called at its toplevel;
@@ -1121,13 +1171,19 @@ and parser_cont : type s tr tr' a r.
            is retried with « "{"; same-entry-at-top-level; "}" », allowing
            e.g. to parse « {1 + 1} » while « {(1 + 1)} » would
            have been expected according to the level. *)
+      if gstate.recover then
         let p1 = parser_of_tree entry nlevn alevn son in
-        let a = continue_parser_of_entry gstate (entry_of_symb entry s) 0 bp a strm__ in
+        let a = continue_parser_of_entry gstate (entry_of_symb entry s) None 0 bp a strm__ in
         let act =
           try p1 gstate strm__ with
             Stream.Failure -> raise (Error (tree_failed entry a s son))
         in
-        fun _ -> act a
+        fun _ ->
+          warn_recover nlevn alevn (Capsule (entry, s)) gstate bp strm__;
+          act a
+
+      else
+        raise (Error (tree_failed entry a s son))
 
 (** [parser_of_token_list] attempts to look-ahead an arbitrary-long
 finite sequence of tokens. E.g., in
@@ -1171,7 +1227,14 @@ and parser_of_token_list : type s tr lt r.
          match
            try Some (ps gstate strm) with Stream.Failure ->
            (* Tolerance: retry w/o granting the level constraint (see recover) *)
-           try Some (parser_of_tree entry nlevn alevn (top_tree entry tree) gstate strm) with Stream.Failure -> None
+           if gstate.recover then
+             try
+               let bp = LStream.count strm in
+               let a = Some (parser_of_tree entry nlevn alevn (top_tree entry tree) gstate strm) in
+               warn_recover nlevn alevn (get_node entry tree) gstate bp strm; a
+             with Stream.Failure -> None
+           else
+             None
          with
          | Some act -> act
          | None -> raise (TokenListFailed (entry, last_a, (Stoken last_tok), tree))
@@ -1398,7 +1461,7 @@ let rec start_parser_of_levels entry clevn =
                  let act = p2 gstate strm__ in
                  let ep = LStream.count strm__ in
                  let a = act (LStream.interval_loc bp ep strm__) in
-                 continue_parser_of_entry gstate entry levn bp a strm)
+                 continue_parser_of_entry gstate entry (Some clevn) levn bp a strm)
           | _ ->
               fun gstate levn strm ->
                 if levn > clevn then
@@ -1411,7 +1474,7 @@ let rec start_parser_of_levels entry clevn =
                     Some act ->
                       let ep = LStream.count strm__ in
                       let a = act (LStream.interval_loc bp ep strm__) in
-                      continue_parser_of_entry gstate entry levn bp a strm
+                      continue_parser_of_entry gstate entry (Some clevn) levn bp a strm
                   | _ -> p1 gstate levn strm__
 
 (** [continue_parser_of_levels entry clevn levels levn bp a strm] goes
@@ -1427,7 +1490,7 @@ let rec start_parser_of_levels entry clevn =
 *)
 let rec continue_parser_of_levels entry clevn =
   function
-    [] -> (fun _gstate levn bp a (strm__ : _ LStream.t) -> raise Stream.Failure)
+    [] -> (fun _gstate levfrom levn bp a (strm__ : _ LStream.t) -> raise Stream.Failure)
   | Level lev :: levs ->
       let p1 = continue_parser_of_levels entry (succ clevn) levs in
       match lev.lsuffix with
@@ -1439,27 +1502,41 @@ let rec continue_parser_of_levels entry clevn =
             | RightA -> clevn
           in
           let p2 = parser_of_tree entry (succ clevn) alevn tree in
-          fun gstate levn bp a strm ->
+          fun gstate levfrom levn bp a strm ->
+            (* Apply the lsuffix continuation if the level is in the interval [levn;levfrom] *)
             if levn > clevn then
               (* Skip rules before [levn] *)
-              p1 gstate levn bp a strm
+              p1 gstate levfrom levn bp a strm
+            else if (not gstate.recover && match levfrom with Some levfrom -> levfrom < clevn | None -> false) then
+              raise Stream.Failure
             else
               let (strm__ : _ LStream.t) = strm in
-              try p1 gstate levn bp a strm__ with
+              let ep = LStream.count strm__ in
+              let c = try p1 gstate levfrom levn bp a strm__ with
                 Stream.Failure ->
                   let act = p2 gstate strm__ in
                   let ep = LStream.count strm__ in
                   let a = act a (LStream.interval_loc bp ep strm__) in
-                  continue_parser_of_entry gstate entry levn bp a strm
+                  if gstate.has_non_assoc && lev.assoc = NonA then
+                    if clevn = levn then
+                      a
+                    else
+                      continue_parser_of_entry gstate entry (Some (clevn-1)) levn bp a strm
+                  else
+                    continue_parser_of_entry gstate entry (Some clevn) levn bp a strm in
+              let () =
+                if match levfrom with Some levfrom -> levfrom < clevn | None -> false then
+                  warn_recover_continuation bp ep strm__ in
+              c
 
 let make_continue_parser_of_entry entry desc =
   match desc with
-  | Dlevels [] -> (fun _ _ _ _ (_ : _ LStream.t) -> raise Stream.Failure)
+  | Dlevels [] -> (fun _ _ _ _ _ (_ : _ LStream.t) -> raise Stream.Failure)
   | Dlevels elev ->
     let p = lazy (continue_parser_of_levels entry 0 elev) in
-    (fun gstate levn bp a (strm__ : _ LStream.t) ->
-       try Lazy.force p gstate levn bp a strm__ with Stream.Failure -> a)
-  | Dparser p -> fun gstate levn bp a (strm__ : _ LStream.t) -> raise Stream.Failure
+    (fun gstate levfrom levn bp a (strm__ : _ LStream.t) ->
+       try Lazy.force p gstate levfrom levn bp a strm__ with Stream.Failure -> a)
+  | Dparser p -> fun gstate levfrom levn bp a (strm__ : _ LStream.t) -> raise Stream.Failure
 
 let make_start_parser_of_entry entry desc =
   match desc with
@@ -1572,7 +1649,7 @@ module Entry = struct
     eentry = e;
     edesc = Dlevels [];
     estart = empty_entry e.ename;
-    econtinue = (fun _ _ _ _ (strm__ : _ LStream.t) -> raise Stream.Failure);
+    econtinue = (fun _ _ _ _ _ (strm__ : _ LStream.t) -> raise Stream.Failure);
   }
 
   let make n estate =
@@ -1591,7 +1668,7 @@ module Entry = struct
   let of_parser_val e { parser_fun = p } = {
     eentry = e;
     estart = (fun gstate _ (strm:_ LStream.t) -> p gstate.kwstate strm);
-    econtinue = (fun _ _ _ _ (strm__ : _ LStream.t) -> raise Stream.Failure);
+    econtinue = (fun _ _ _ _ _ (strm__ : _ LStream.t) -> raise Stream.Failure);
     edesc = Dparser p;
   }
   let of_parser n p estate =
diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli
index 56ffb6f3f84c..11b3417c6cf6 100644
--- a/gramlib/grammar.mli
+++ b/gramlib/grammar.mli
@@ -143,6 +143,8 @@ module type ExtS = sig
     type t = {
       estate : EState.t;
       kwstate : keyword_state;
+      recover : bool;
+      has_non_assoc : bool;
     }
   end
 
diff --git a/parsing/procq.ml b/parsing/procq.ml
index eb4ddb219d51..a04d93cb3432 100644
--- a/parsing/procq.ml
+++ b/parsing/procq.ml
@@ -41,7 +41,7 @@ type full_state = {
 }
 
 let empty_full_state =
-  let empty_gstate = { GState.estate = EState.empty; kwstate = CLexer.empty_keyword_state } in
+  let empty_gstate = { GState.estate = EState.empty; kwstate = CLexer.empty_keyword_state; recover = true; has_non_assoc = false } in
   {
     current_state = empty_gstate;
     base_state = empty_gstate;
@@ -76,7 +76,7 @@ let modify_state_unsync f state =
 let modify_state_unsync f () = state := modify_state_unsync f !state
 
 let modify_keyword_state f =
-  modify_state_unsync (fun {estate;kwstate} -> {estate; kwstate = f kwstate})
+  modify_state_unsync (fun {estate;kwstate;recover;has_non_assoc} -> {estate; kwstate = f kwstate; recover; has_non_assoc})
     ()
 
 let make_entry_unsync make remake state =
@@ -98,17 +98,17 @@ let add_kw = { add_kw = CLexer.add_keyword_tok }
 
 let epsilon_value (type s tr a) f (e : (s, tr, a) Symbol.t) =
   let r = Production.make (Rule.next Rule.stop e) (fun x _ -> f x) in
-  let { GState.estate; kwstate } = gstate() in
+  let { GState.estate; kwstate; recover; has_non_assoc } = gstate() in
   let estate, entry = Entry.make "epsilon" estate in
   let ext = Fresh (Gramlib.Gramext.First, [None, None, [r]]) in
   let estate, kwstate = safe_extend add_kw estate kwstate entry ext in
   let strm = Stream.empty () in
   let strm = Parsable.make strm in
-  try Some (Entry.parse entry strm {estate;kwstate}) with e when CErrors.noncritical e -> None
+  try Some (Entry.parse entry strm {estate;kwstate;recover;has_non_assoc}) with e when CErrors.noncritical e -> None
 
-let extend_gstate {GState.kwstate; estate} e ext =
+let extend_gstate {GState.kwstate; estate; recover; has_non_assoc} e ext =
   let estate, kwstate = safe_extend add_kw estate kwstate e ext in
-  {GState.kwstate; estate}
+  {GState.kwstate; estate; recover; has_non_assoc}
 
 (* XXX rename to grammar_extend_unsync? *)
 let grammar_extend e ext =
diff --git a/test-suite/bugs/bug_11866.v b/test-suite/bugs/bug_11866.v
index 8ebcc0992a24..71c5c0fa8a98 100644
--- a/test-suite/bugs/bug_11866.v
+++ b/test-suite/bugs/bug_11866.v
@@ -25,19 +25,23 @@ Goal True.
   ex5 :::0 0 +0 0.
   ex6 :::0 0 +0 0.
 
-  ex0 :::1 0 +1 0.
+  (*ex0 :::1 0 +1 0.*)
   ex1 :::1 0 +1 0.
   (*ex2 :::1 0 +1 0.*)
   (*ex3 :::1 0 +1 0.*)
   ex4 :::1 0 +1 0.
+  ex4 :::4 0 +4 0.
+  (*ex4 :::5 0 +5 0.*)
   ex5 :::1 0 +1 0.
+  ex5 :::5 0 +5 0.
+  (*ex5 :::6 0 +6 0.*)
   ex6 :::1 0 +1 0.
 
-  ex0 :::6 0 +6 0.
-  ex1 :::6 0 +6 0.
+  (*ex0 :::6 0 +6 0.*)
+  (*ex1 :::6 0 +6 0.*)
   (*ex2 :::6 0 +6 0.*)
   (*ex3 :::6 0 +6 0.*)
-  ex4 :::6 0 +6 0.
-  ex5 :::6 0 +6 0.
+  (*ex4 :::6 0 +6 0.*)
+  (*ex5 :::6 0 +6 0.*)
   ex6 :::6 0 +6 0.
 Abort.
diff --git a/test-suite/bugs/bug_3427.v b/test-suite/bugs/bug_3427.v
index ef09a01370d5..701659497425 100644
--- a/test-suite/bugs/bug_3427.v
+++ b/test-suite/bugs/bug_3427.v
@@ -116,7 +116,7 @@ Global Instance isequiv_ap_hproptype `{Funext} X Y : IsEquiv (@ap _ _ hproptype
 admit.
 Defined.
 
-Definition path_hprop `{Funext} X Y := (@ap _ _ hproptype X Y)^-1%equiv.
+Definition path_hprop `{Funext} X Y := ((@ap _ _ hproptype X Y)^-1)%equiv.
 
 Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}.
 Local Open Scope equiv_scope.
diff --git a/test-suite/bugs/bug_4116.v b/test-suite/bugs/bug_4116.v
index 4027b0979844..31d967664996 100644
--- a/test-suite/bugs/bug_4116.v
+++ b/test-suite/bugs/bug_4116.v
@@ -351,7 +351,7 @@ Section Grothendieck2.
       intro m.
       transparent assert (H' : (s.(c) = d.(c))).
       {
-        apply (idtoiso C (x := s.(c)) (y := d.(c)))^-1%function.
+        apply ((idtoiso C (x := s.(c)) (y := d.(c)))^-1)%function.
         exists (m : morphism _ _ _).1.
         admit.
 
diff --git a/test-suite/bugs/bug_9521.v b/test-suite/bugs/bug_9521.v
index 2c7cbb4335be..d4f3f9891f18 100644
--- a/test-suite/bugs/bug_9521.v
+++ b/test-suite/bugs/bug_9521.v
@@ -4,7 +4,7 @@ Declare Custom Entry expr.
 Module A.
 
 Notation "expr0:( s )" := s (s custom expr at level 0).
-Notation "#" := 0 (in custom expr at level 1).
+Notation "#" := 0 (in custom expr at level 0).
 Check expr0:(#). (* Should not be an anomaly "unknown level 0" *)
 
 End A.
diff --git a/test-suite/ltac2/control_tests.v b/test-suite/ltac2/control_tests.v
index 3c51ee9a16aa..a049f2435fec 100644
--- a/test-suite/ltac2/control_tests.v
+++ b/test-suite/ltac2/control_tests.v
@@ -84,7 +84,7 @@ Goal True /\ False.
   split.
   let r := ref 0 in
   enter (fun () =>
-           if Int.equal (get r) 0 then incr r; exact I
+           if Int.equal (get r) 0 then (incr r; exact I)
            else ()).
   all: if Int.equal (numgoals()) 1 then () else throw Error.
 Abort.
diff --git a/test-suite/ltac2/fragile_matching.v b/test-suite/ltac2/fragile_matching.v
index 16423a48a684..f494fae91c36 100644
--- a/test-suite/ltac2/fragile_matching.v
+++ b/test-suite/ltac2/fragile_matching.v
@@ -62,7 +62,7 @@ Module RealCodeTest.
   Ltac2 Type interface := { dirty : unit -> bool }.
 
   Ltac2 useForm () := {
-    dirty := fun () =>
+    dirty := (fun () =>
       Array.for_all
         (fun item =>
           match item with
@@ -109,7 +109,7 @@ Module RealCodeTest.
             } =>
             true
           end)
-        Array.empty
+        Array.empty)
     }.
 
 End RealCodeTest.
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index ef2a69ca1ba2..d560e682d227 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -212,7 +212,7 @@ Notation NONE3 := @None.
 Notation SOME3 := @Some.
 Check (fun x => match x with SOME3 _ x => x | NONE3 _ => 0 end).
 
-Notation "a :'" := (cons a) (at level 12).
+Notation "a :'" := (cons a) (at level 10).
 
 Check (fun x => match x with | nil => NONE | h :' t => SOME3 _ t end).
 
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index a340714f584c..9aef5358a67c 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -88,28 +88,28 @@ where
   |- Type] (pat, p0, p cannot be used)
 fun '{| |} => true
      : R -> bool
-File "./output/Notations4.v", line 149, characters 82-85:
+File "./output/Notations4.v", line 147, characters 82-85:
 The command has indeed failed with message:
 The format is not the same on the right- and left-hand sides of the special token "..".
-File "./output/Notations4.v", line 153, characters 76-78:
+File "./output/Notations4.v", line 151, characters 76-78:
 The command has indeed failed with message:
 The format is not the same on the right- and left-hand sides of the special token "..".
-File "./output/Notations4.v", line 157, characters 78-81:
+File "./output/Notations4.v", line 155, characters 78-81:
 The command has indeed failed with message:
 The format is not the same on the right- and left-hand sides of the special token "..".
-File "./output/Notations4.v", line 161, characters 52-55:
+File "./output/Notations4.v", line 159, characters 52-55:
 The command has indeed failed with message:
 The format is not the same on the right- and left-hand sides of the special token "..".
-File "./output/Notations4.v", line 167, characters 35-39:
+File "./output/Notations4.v", line 165, characters 35-39:
 Warning: Accessing custom entry B.expr by its unqualified name is deprecated.
 [deprecated-unqualified-custom-entry,deprecated-since-9.2,deprecated,default]
 Quickfix:
-Replace File "./output/Notations4.v", line 167, characters 35-39 with B.expr
-File "./output/Notations4.v", line 168, characters 21-25:
+Replace File "./output/Notations4.v", line 165, characters 35-39 with B.expr
+File "./output/Notations4.v", line 166, characters 21-25:
 Warning: Accessing custom entry B.expr by its unqualified name is deprecated.
 [deprecated-unqualified-custom-entry,deprecated-since-9.2,deprecated,default]
 Quickfix:
-Replace File "./output/Notations4.v", line 168, characters 21-25 with B.expr
+Replace File "./output/Notations4.v", line 166, characters 21-25 with B.expr
 Entry custom:Notations4.B.expr is
 [ "201" RIGHTA
   [ "{"; term LEVEL "200"; "}" ] ]
@@ -120,18 +120,18 @@ fun x : nat => [x]
      : nat -> nat
 ∀ x : nat, x = x
      : Prop
-File "./output/Notations4.v", line 195, characters 0-160:
+File "./output/Notations4.v", line 193, characters 0-160:
 Warning: Notation "∀ _ .. _ , _" was already defined with a different format
 in scope type_scope. [notation-incompatible-format,parsing,default]
 ∀x : nat,x = x
      : Prop
-File "./output/Notations4.v", line 208, characters 0-60:
+File "./output/Notations4.v", line 206, characters 0-60:
 Warning: Notation "_ %%% _" was already defined with a different format.
 [notation-incompatible-format,parsing,default]
-File "./output/Notations4.v", line 212, characters 0-64:
+File "./output/Notations4.v", line 210, characters 0-64:
 Warning: Notation "_ %%% _" was already defined with a different format.
 [notation-incompatible-format,parsing,default]
-File "./output/Notations4.v", line 217, characters 0-62:
+File "./output/Notations4.v", line 215, characters 0-62:
 Warning: Lonely notation "_ %%%% _" was already defined with a different
 format. [notation-incompatible-format,parsing,default]
 3  %%  4
@@ -140,10 +140,10 @@ format. [notation-incompatible-format,parsing,default]
      : nat
 3   %%   4
      : nat
-File "./output/Notations4.v", line 245, characters 47-59:
+File "./output/Notations4.v", line 243, characters 47-59:
 Warning: The format modifier is irrelevant for only-parsing rules.
 [irrelevant-format-only-parsing,parsing,default]
-File "./output/Notations4.v", line 249, characters 36-48:
+File "./output/Notations4.v", line 247, characters 36-48:
 Warning: The only parsing modifier has no effect in Reserved Notation.
 [irrelevant-reserved-notation-only-parsing,parsing,default]
 fun x : nat => U (S x)
@@ -154,7 +154,7 @@ fun x : nat => V x
      : forall x : nat, nat * (?T -> ?T)
 where
 ?T : [x : nat |- Type]
-File "./output/Notations4.v", line 266, characters 0-30:
+File "./output/Notations4.v", line 264, characters 0-30:
 Warning: Notation "_ :=: _" was already used.
 [notation-overridden,parsing,default]
 0 :=: 0
@@ -171,49 +171,49 @@ exists p : nat, ▢_p (p >= 1)
      : Prop
 ▢_n (n >= 1)
      : Prop
-File "./output/Notations4.v", line 336, characters 17-20:
+File "./output/Notations4.v", line 334, characters 17-20:
 The command has indeed failed with message:
 Found an inductive type while a variable name was expected.
-File "./output/Notations4.v", line 337, characters 17-18:
+File "./output/Notations4.v", line 335, characters 17-18:
 The command has indeed failed with message:
 Found a constructor while a variable name was expected.
-File "./output/Notations4.v", line 339, characters 17-18:
+File "./output/Notations4.v", line 337, characters 17-18:
 The command has indeed failed with message:
 Found a constant while a variable name was expected.
 exists x y : nat, ▢_(x, y) (x >= 1 /\ y >= 2)
      : Prop
 ▢_n (n >= 1)
      : Prop
-File "./output/Notations4.v", line 352, characters 17-20:
+File "./output/Notations4.v", line 350, characters 17-20:
 The command has indeed failed with message:
 Found an inductive type while a pattern was expected.
 ▢_tt (tt = tt)
      : Prop
-File "./output/Notations4.v", line 355, characters 17-18:
+File "./output/Notations4.v", line 353, characters 17-18:
 The command has indeed failed with message:
 Found a constant while a pattern was expected.
 exists x y : nat, ▢_(x, y) (x >= 1 /\ y >= 2)
      : Prop
 pseudo_force n (fun n : nat => n >= 1)
      : Prop
-File "./output/Notations4.v", line 368, characters 17-20:
+File "./output/Notations4.v", line 366, characters 17-20:
 The command has indeed failed with message:
 Found an inductive type while a pattern was expected.
 ▢_tt (tt = tt)
      : Prop
-File "./output/Notations4.v", line 371, characters 17-18:
+File "./output/Notations4.v", line 369, characters 17-18:
 The command has indeed failed with message:
 Found a constant while a pattern was expected.
 exists x y : nat, myforce (x, y) (x >= 1 /\ y >= 2)
      : Prop
 myforce n (n >= 1)
      : Prop
-File "./output/Notations4.v", line 383, characters 21-24:
+File "./output/Notations4.v", line 381, characters 21-24:
 The command has indeed failed with message:
 Found an inductive type while a pattern was expected.
 myforce tt (tt = tt)
      : Prop
-File "./output/Notations4.v", line 386, characters 21-22:
+File "./output/Notations4.v", line 384, characters 21-22:
 The command has indeed failed with message:
 Found a constant while a pattern was expected.
 id nat
@@ -222,7 +222,7 @@ fun a : bool => id a
      : bool -> bool
 fun nat : bool => id nat
      : bool -> bool
-File "./output/Notations4.v", line 398, characters 17-20:
+File "./output/Notations4.v", line 396, characters 17-20:
 The command has indeed failed with message:
 Found an inductive type while a pattern was expected.
 !! nat, nat = true
@@ -251,7 +251,7 @@ Found an inductive type while a pattern was expected.
      : Type
 ## (x, _) (x = 0)
      : Prop
-File "./output/Notations4.v", line 494, characters 21-30:
+File "./output/Notations4.v", line 492, characters 21-30:
 The command has indeed failed with message:
 Unexpected type constraint in notation already providing a type constraint.
 ## '(x, y) (x + y = 0)
@@ -284,12 +284,12 @@ where
 ?A : [ |- Type]
 0
      : nat
-File "./output/Notations4.v", line 544, characters 0-78:
+File "./output/Notations4.v", line 542, characters 0-78:
 The command has indeed failed with message:
 Notation "func _ .. _ , _" is already defined at level 200 with arguments
 binder, constr at next level while it is now required to be at level 200
 with arguments constr, constr at next level.
-File "./output/Notations4.v", line 549, characters 0-57:
+File "./output/Notations4.v", line 547, characters 0-57:
 The command has indeed failed with message:
 Notation "[[ _ ]]" is already defined at level 0 with arguments custom foo
 while it is now required to be at level 0 with arguments custom bar.
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 8870c92cd69e..2eba1dee25d5 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -80,11 +80,9 @@ Notation "x + y" := (Add x y) (in custom expr at level 2, left associativity).
 Notation "( x )" := x (in custom expr at level 0, x at level 2).
 
 (* Check the use of a two-steps coercion from constr to expr 1 then
-   from expr 0 to expr 2 (note that camlp5 parsing is more tolerant
-   and does not require parentheses to parse from level 2 while at
-   level 1) *)
+   from expr 0 to expr 2 *)
 
-Check [1 + 1].
+Check [(1 + 1)].
 
 End C.
 
diff --git a/theories/Corelib/BinNums/PosDef.v b/theories/Corelib/BinNums/PosDef.v
index fe2cdb5f3a22..fd91e24f5fc8 100644
--- a/theories/Corelib/BinNums/PosDef.v
+++ b/theories/Corelib/BinNums/PosDef.v
@@ -28,10 +28,8 @@ Local Open Scope positive_scope.
     for the number 6 (which is 110 in binary notation).
 *)
 
-Notation "p ~ 1" := (xI p)
- (at level 7, left associativity, format "p '~' '1'") : positive_scope.
-Notation "p ~ 0" := (xO p)
- (at level 7, left associativity, format "p '~' '0'") : positive_scope.
+Notation "p ~ 1" := (xI p) (format "p '~' '1'") : positive_scope.
+Notation "p ~ 0" := (xO p) (format "p '~' '0'") : positive_scope.
 
 Notation "1" := xH : positive_scope.
 Notation "2" := 1~0 : positive_scope.