Merge PR #12984: [printing] Order notations by matching precision first, and then by last imported

Reviewed-by: Zimmi48
Ack-by: RalfJung
Ack-by: gares

16 files changed, 427 insertions, 114 deletions

diff --git a/clib/cArray.ml b/clib/cArray.ml
index 7249bcada0..95ae48a7ba 100644
--- a/clib/cArray.ml
+++ b/clib/cArray.ml
@@ -56,6 +56,7 @@ sig
     (int -> 'a -> 'b -> 'c -> 'd) -> 'a array -> 'b array -> 'c array -> 'd array
   val map_left : ('a -> 'b) -> 'a array -> 'b array
   val iter2_i : (int -> 'a -> 'b -> unit) -> 'a array -> 'b array -> unit
+  val iter3 : ('a -> 'b -> 'c -> unit) -> 'a array -> 'b array -> 'c array -> unit
   val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b array -> 'a * 'c array
   val fold_right_map : ('a -> 'c -> 'b * 'c) -> 'a array -> 'c -> 'b array * 'c
   val fold_left2_map : ('a -> 'b -> 'c -> 'a * 'd) -> 'a -> 'b array -> 'c array -> 'a * 'd array
@@ -392,6 +393,13 @@ let iter2_i f v1 v2 =
   let () = if not (Int.equal len2 len1) then invalid_arg "Array.iter2" in
   for i = 0 to len1 - 1 do f i (uget v1 i) (uget v2 i) done
 
+let iter3 f v1 v2 v3 =
+  let len1 = Array.length v1 in
+  let len2 = Array.length v2 in
+  let len3 = Array.length v3 in
+  let () = if not (Int.equal len2 len1) || not (Int.equal len1 len3) then invalid_arg "Array.iter3" in
+  for i = 0 to len1 - 1 do f (uget v1 i) (uget v2 i) (uget v3 i) done
+
 let map_right f a =
   let l = length a in
   if l = 0 then [||] else begin
diff --git a/clib/cArray.mli b/clib/cArray.mli
index f40ceb56db..664bad4c0a 100644
--- a/clib/cArray.mli
+++ b/clib/cArray.mli
@@ -92,6 +92,9 @@ sig
   val iter2_i : (int -> 'a -> 'b -> unit) -> 'a array -> 'b array -> unit
   (** Iter on two arrays. Raise [Invalid_argument "Array.iter2_i"] if sizes differ. *)
 
+  val iter3 : ('a -> 'b -> 'c -> unit) -> 'a array -> 'b array -> 'c array -> unit
+  (** Iter on three arrays. Raise [Invalid_argument "Array.iter3"] if sizes differ. *)
+
   val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b array -> 'a * 'c array
   (** [fold_left_map f e_0 [|l_1...l_n|] = e_n,[|k_1...k_n|]]
     where [(e_i,k_i)=f e_{i-1} l_i]; see also [Smart.fold_left_map] *)
diff --git a/doc/changelog/03-notations/12984-master+import-notation-make-active-again.rst b/doc/changelog/03-notations/12984-master+import-notation-make-active-again.rst
new file mode 100644
index 0000000000..d472e6fdf0
--- /dev/null
+++ b/doc/changelog/03-notations/12984-master+import-notation-make-active-again.rst
@@ -0,0 +1,12 @@
+- **Changed:**
+  Redeclaring a notation reactivates also its printing rule; in
+  particular a second :cmd:`Import` of the same module reactivates the
+  printing rules declared in this module. In theory, this leads to
+  changes of behavior for printing. However, this is mitigated in
+  general by the adoption in `#12986
+  <https://github.com/coq/coq/pull/12986>`_ of a priority given to
+  notations which match a larger part of the term to print
+  (`#12984 <https://github.com/coq/coq/pull/12984>`_,
+  fixes `#7443 <https://github.com/coq/coq/issues/7443>`_
+  and `#10824 <https://github.com/coq/coq/issues/10824>`_,
+  by Hugo Herbelin).
diff --git a/doc/changelog/03-notations/12986-master+ordering-notation-by-precision.rst b/doc/changelog/03-notations/12986-master+ordering-notation-by-precision.rst
new file mode 100644
index 0000000000..8b233972bf
--- /dev/null
+++ b/doc/changelog/03-notations/12986-master+ordering-notation-by-precision.rst
@@ -0,0 +1,5 @@
+- **Changed:**
+  Use of notations for printing now gives preference
+  to notations which match a larger part of the term to abbreviate
+  (`#12986 <https://github.com/coq/coq/pull/12986>`_,
+  by Hugo Herbelin).
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 56b14d0935..16c8586a9f 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -214,7 +214,7 @@ have to be observed for notations starting with a symbol, e.g., rules
 starting with “\ ``{``\ ” or “\ ``(``\ ” should be put at level 0. The list
 of Coq predefined notations can be found in the chapter on :ref:`thecoqlibrary`.
 
-Displaying symbolic notations
+Use of notations for printing
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 The command :cmd:`Notation` has an effect both on the Coq parser and on the
@@ -323,6 +323,26 @@ at the time of use of the notation.
    scope. Obviously, expressions printed by means of such extra
    printing rules will not be reparsed to the same form.
 
+.. note::
+
+   When several notations can be used to print a given term, the
+   notations which capture the largest subterm of the term are used
+   preferentially. Here is an example:
+
+   .. coqtop:: in
+
+     Notation "x < y" := (lt x y) (at level 70).
+     Notation "x < y < z" := (lt x y /\ lt y z) (at level 70, y at next level).
+
+     Check (0 < 1 /\ 1 < 2).
+
+   When several notations match the same subterm, or incomparable
+   subterms of the term to print, the notation declared most recently
+   is selected. Moreover, reimporting a library or module declares the
+   notations of this library or module again. If the notation is in a
+   scope (see :ref:`Scopes`), either the scope has to be opened or a
+   delimiter has to exist in the scope for the notation to be usable.
+
 The Infix command
 ~~~~~~~~~~~~~~~~~~
 
diff --git a/interp/notation.ml b/interp/notation.ml
index 1a361dc1a6..286ece6cb6 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -345,11 +345,23 @@ let also_cases_notation_rule_eq (also_cases1,rule1) (also_cases2,rule2) =
   (* No need in principle to compare also_cases as it is inferred *)
   also_cases1 = also_cases2 && notation_rule_eq rule1 rule2
 
+let adjust_application c1 c2 =
+  match c1, c2 with
+  | NApp (t1, a1), (NList (_,_,NApp (_, a2),_,_) | NApp (_, a2)) when List.length a1 >= List.length a2 ->
+      NApp (t1, List.firstn (List.length a2) a1)
+  | NApp (t1, a1), _ ->
+      t1
+  | _ -> c1
+
+let strictly_finer_interpretation_than (_,(_,(vars1,c1),_)) (_,(_,(vars2,c2),_)) =
+  let c1 = adjust_application c1 c2 in
+  Notation_ops.strictly_finer_notation_constr (List.map fst vars1, List.map fst vars2) c1 c2
+
 let keymap_add key interp map =
   let old = try KeyMap.find key map with Not_found -> [] in
-  (* In case of re-import, no need to keep the previous copy *)
-  let old = try List.remove_first (also_cases_notation_rule_eq interp) old with Not_found -> old in
-  KeyMap.add key (interp :: old) map
+  (* strictly finer interpretation are kept in front *)
+  let strictly_finer, rest = List.partition (fun c -> strictly_finer_interpretation_than c interp) old in
+  KeyMap.add key (strictly_finer @ interp :: rest) map
 
 let keymap_remove key interp map =
   let old = try KeyMap.find key map with Not_found -> [] in
@@ -1419,12 +1431,12 @@ let check_parsing_override (scopt,ntn) data = function
   | OnlyParsingData (_,old_data) ->
     let overridden = not (interpretation_eq data.not_interp old_data.not_interp) in
     warn_override_if_needed (scopt,ntn) overridden data old_data;
-    None, not overridden
+    None
   | ParsingAndPrintingData (_,on_printing,old_data) ->
     let overridden = not (interpretation_eq data.not_interp old_data.not_interp) in
     warn_override_if_needed (scopt,ntn) overridden data old_data;
-    (if on_printing then Some old_data.not_interp else None), not overridden
-  | NoParsingData -> None, false
+    if on_printing then Some old_data.not_interp else None
+  | NoParsingData -> None
 
 let check_printing_override (scopt,ntn) data parsingdata printingdata =
   let parsing_update = match parsingdata with
@@ -1453,15 +1465,15 @@ let update_notation_data (scopt,ntn) use data table =
     try NotationMap.find ntn table with Not_found -> (NoParsingData, []) in
   match use with
   | OnlyParsing ->
-    let printing_update, exists = check_parsing_override (scopt,ntn) data parsingdata in
-    NotationMap.add ntn (OnlyParsingData (true,data), printingdata) table, printing_update, exists
+    let printing_update = check_parsing_override (scopt,ntn) data parsingdata in
+    NotationMap.add ntn (OnlyParsingData (true,data), printingdata) table, printing_update
   | ParsingAndPrinting ->
-    let printing_update, exists = check_parsing_override (scopt,ntn) data parsingdata in
-    NotationMap.add ntn (ParsingAndPrintingData (true,true,data), printingdata) table, printing_update, exists
+    let printing_update = check_parsing_override (scopt,ntn) data parsingdata in
+    NotationMap.add ntn (ParsingAndPrintingData (true,true,data), printingdata) table, printing_update
   | OnlyPrinting ->
     let parsingdata, exists = check_printing_override (scopt,ntn) data parsingdata printingdata in
     let printingdata = if exists then printingdata else (true,data) :: printingdata in
-    NotationMap.add ntn (parsingdata, printingdata) table, None, exists
+    NotationMap.add ntn (parsingdata, printingdata) table, None
 
 let rec find_interpretation ntn find = function
   | [] -> raise Not_found
@@ -1734,23 +1746,22 @@ let declare_notation (scopt,ntn) pat df ~use ~also_in_cases_pattern coe deprecat
     not_location = df;
     not_deprecation = deprecation;
   } in
-  let notation_update,printing_update, exists = update_notation_data (scopt,ntn) use notdata sc.notations in
-  if not exists then
-    let sc = { sc with notations = notation_update } in
-    scope_map := String.Map.add scope sc !scope_map;
+  let notation_update,printing_update = update_notation_data (scopt,ntn) use notdata sc.notations in
+  let sc = { sc with notations = notation_update } in
+  scope_map := String.Map.add scope sc !scope_map;
   (* Update the uninterpretation cache *)
   begin match printing_update with
   | Some pat -> remove_uninterpretation (NotationRule (scopt,ntn)) also_in_cases_pattern pat
   | None -> ()
   end;
-  if not exists && use <> OnlyParsing then declare_uninterpretation ~also_in_cases_pattern (NotationRule (scopt,ntn)) pat;
+  if use <> OnlyParsing then declare_uninterpretation ~also_in_cases_pattern (NotationRule (scopt,ntn)) pat;
   (* Register visibility of lonely notations *)
-  if not exists then begin match scopt with
+  begin match scopt with
   | LastLonelyNotation -> scope_stack := LonelyNotationItem ntn :: !scope_stack
   | NotationInScope _ -> ()
   end;
   (* Declare a possible coercion *)
-  if not exists then begin match coe with
+  begin match coe with
    | Some (IsEntryCoercion entry) ->
      let (_,level,_) = level_of_notation ntn in
      let level = match fst ntn with
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 7cb3ca25ee..d393dcaecb 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -24,82 +24,182 @@ open Notation_term
 (**********************************************************************)
 (* Utilities                                                          *)
 
-(* helper for NVar, NVar case in eq_notation_constr *)
-let get_var_ndx id vs = try Some (List.index Id.equal id vs) with Not_found -> None
-
-let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 =
-(vars1 == vars2 && t1 == t2) ||
-match t1, t2 with
-| NRef gr1, NRef gr2 -> GlobRef.equal gr1 gr2
-| NVar id1, NVar id2 -> (
-   match (get_var_ndx id1 vars1,get_var_ndx id2 vars2) with
-   | Some n,Some m -> Int.equal n m
-   | None  ,None   -> Id.equal id1 id2
-   | _             -> false)
-| NApp (t1, a1), NApp (t2, a2) ->
-  (eq_notation_constr vars) t1 t2 && List.equal (eq_notation_constr vars) a1 a2
-| NHole (_, _, _), NHole (_, _, _) -> true (* FIXME? *)
-| NList (i1, j1, t1, u1, b1), NList (i2, j2, t2, u2, b2) ->
-  Id.equal i1 i2 && Id.equal j1 j2 && (eq_notation_constr vars) t1 t2 &&
-  (eq_notation_constr vars) u1 u2 && b1 == b2
-| NLambda (na1, t1, u1), NLambda (na2, t2, u2) ->
-  Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2
-| NProd (na1, t1, u1), NProd (na2, t2, u2) ->
-  Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2
-| NBinderList (i1, j1, t1, u1, b1), NBinderList (i2, j2, t2, u2, b2) ->
-  Id.equal i1 i2 && Id.equal j1 j2 && (eq_notation_constr vars) t1 t2 &&
-  (eq_notation_constr vars) u1 u2 && b1 == b2
-| NLetIn (na1, b1, t1, u1), NLetIn (na2, b2, t2, u2) ->
-  Name.equal na1 na2 && eq_notation_constr vars b1 b2 &&
-  Option.equal (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2
-| NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (* FIXME? *)
-  let eqpat (p1, t1) (p2, t2) =
-    List.equal cases_pattern_eq p1 p2 &&
-    (eq_notation_constr vars) t1 t2
-  in
-  let eqf (t1, (na1, o1)) (t2, (na2, o2)) =
-    let eq (i1, n1) (i2, n2) = Ind.CanOrd.equal i1 i2 && List.equal Name.equal n1 n2 in
-    (eq_notation_constr vars) t1 t2 && Name.equal na1 na2 && Option.equal eq o1 o2
-  in
-  Option.equal (eq_notation_constr vars) o1 o2 &&
-  List.equal eqf r1 r2 &&
-  List.equal eqpat p1 p2
-| NLetTuple (nas1, (na1, o1), t1, u1), NLetTuple (nas2, (na2, o2), t2, u2) ->
-  List.equal Name.equal nas1 nas2 &&
-  Name.equal na1 na2 &&
-  Option.equal (eq_notation_constr vars) o1 o2 &&
-  (eq_notation_constr vars) t1 t2 &&
-  (eq_notation_constr vars) u1 u2
-| NIf (t1, (na1, o1), u1, r1), NIf (t2, (na2, o2), u2, r2) ->
-  (eq_notation_constr vars) t1 t2 &&
-  Name.equal na1 na2 &&
-  Option.equal (eq_notation_constr vars) o1 o2 &&
-  (eq_notation_constr vars) u1 u2 &&
-  (eq_notation_constr vars) r1 r2
-| NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (* FIXME? *)
-  let eq (na1, o1, t1) (na2, o2, t2) =
-    Name.equal na1 na2 &&
-    Option.equal (eq_notation_constr vars) o1 o2 &&
-    (eq_notation_constr vars) t1 t2
-  in
-  Array.equal Id.equal ids1 ids2 &&
-  Array.equal (List.equal eq) ts1 ts2 &&
-  Array.equal (eq_notation_constr vars) us1 us2 &&
-  Array.equal (eq_notation_constr vars) rs1 rs2
-| NSort s1, NSort s2 ->
-  glob_sort_eq s1 s2
-| NCast (t1, c1), NCast (t2, c2) ->
-  (eq_notation_constr vars) t1 t2 && cast_type_eq (eq_notation_constr vars) c1 c2
-| NInt i1, NInt i2 ->
-   Uint63.equal i1 i2
-| NFloat f1, NFloat f2 ->
-  Float64.equal f1 f2
-| NArray(t1,def1,ty1), NArray(t2,def2,ty2) ->
-  Array.equal (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) def1 def2
-    && eq_notation_constr vars ty1 ty2
-| (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _
-  | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _
-  | NRec _ | NSort _ | NCast _ | NInt _ | NFloat _ | NArray _), _ -> false
+let ldots_var = Id.of_string ".."
+
+let rec alpha_var id1 id2 = function
+  | (i1,i2)::_ when Id.equal i1 id1 -> Id.equal i2 id2
+  | (i1,i2)::_ when Id.equal i2 id2 -> Id.equal i1 id1
+  | _::idl -> alpha_var id1 id2 idl
+  | [] -> Id.equal id1 id2
+
+let cast_type_iter2 f t1 t2 = match t1, t2 with
+  | CastConv t1, CastConv t2 -> f t1 t2
+  | CastVM t1, CastVM t2 -> f t1 t2
+  | CastCoerce, CastCoerce -> ()
+  | CastNative t1, CastNative t2 -> f t1 t2
+  | (CastConv _ | CastVM _ | CastCoerce | CastNative _), _ -> raise Exit
+
+(* used to update the notation variable with the local variables used
+   in NList and NBinderList, since the iterator has its own variable *)
+let replace_var i j var = j :: List.remove Id.equal i var
+
+(* When [lt] is [true], tell if [t1] is a strict refinement of [t2]
+   (this is a partial order, so returning [false] does not mean that
+   [t2] is finer than [t1]); when [lt] is false, tell if [t1] is the
+   same pattern as [t2] *)
+
+let compare_notation_constr lt (vars1,vars2) t1 t2 =
+  (* this is used to reason up to order of notation variables *)
+  let alphameta = ref [] in
+  (* this becomes true when at least one subterm is detected as strictly smaller *)
+  let strictly_lt = ref false in
+  (* this is the stack of inner of iter patterns for comparison with a
+     new iteration or the tail of a recursive pattern *)
+  let tail = ref [] in
+  let check_alphameta id1 id2 =
+    try if not (Id.equal (List.assoc id1 !alphameta) id2) then raise Exit
+    with Not_found ->
+      if (List.mem_assoc id1 !alphameta) then raise Exit;
+      alphameta := (id1,id2) :: !alphameta in
+  let check_eq_id (vars1,vars2) renaming id1 id2 =
+    let ismeta1 = List.mem_f Id.equal id1 vars1 in
+    let ismeta2 = List.mem_f Id.equal id2 vars2 in
+    match ismeta1, ismeta2 with
+    | true, true -> check_alphameta id1 id2
+    | false, false -> if not (alpha_var id1 id2 renaming) then raise Exit
+    | false, true ->
+      if not lt then raise Exit
+      else
+        (* a binder which is not bound in the notation can be
+           considered as strictly more precise since it prevents the
+           notation variables in its scope to be bound by this binder;
+           i.e. it is strictly more precise in the sense that it
+           covers strictly less patterns than a notation where the
+           same binder is bound in the notation; this is hawever
+           disputable *)
+        strictly_lt := true
+    | true, false -> if not lt then raise Exit in
+  let check_eq_name vars renaming na1 na2 =
+    match na1, na2 with
+    | Name id1, Name id2 -> check_eq_id vars renaming id1 id2; (id1,id2)::renaming
+    | Anonymous, Anonymous -> renaming
+    | Anonymous, Name _ when lt -> renaming
+    | _ -> raise Exit in
+  let rec aux (vars1,vars2 as vars) renaming t1 t2 = match t1, t2 with
+  | NVar id1, NVar id2 when id1 = ldots_var && id2 = ldots_var -> ()
+  | _, NVar id2 when lt && id2 = ldots_var -> tail := t1 :: !tail
+  | NVar id1, _ when lt && id1 = ldots_var -> tail := t2 :: !tail
+  | NVar id1, NVar id2 -> check_eq_id vars renaming id1 id2
+  | NHole _, NVar id2 when lt && List.mem_f Id.equal id2 vars2 -> ()
+  | NVar id1, NHole (_, _, _) when lt && List.mem_f Id.equal id1 vars1 -> ()
+  | _, NVar id2 when lt && List.mem_f Id.equal id2 vars2 -> strictly_lt := true
+  | NRef gr1, NRef gr2 when GlobRef.equal gr1 gr2 -> ()
+  | NHole (_, _, _), NHole (_, _, _) -> () (* FIXME? *)
+  | _, NHole (_, _, _) when lt -> strictly_lt := true
+  | NList (i1, j1, iter1, tail1, b1), NList (i2, j2, iter2, tail2, b2)
+  | NBinderList (i1, j1, iter1, tail1, b1), NBinderList (i2, j2, iter2, tail2, b2) ->
+    if b1 <> b2 then raise Exit;
+    let vars1 = replace_var i1 j1 vars1 in
+    let vars2 = replace_var i2 j2 vars2 in
+    check_alphameta i1 i2; aux (vars1,vars2) renaming iter1 iter2; aux vars renaming tail1 tail2;
+  | NBinderList (i1, j1, iter1, tail1, b1), NList (i2, j2, iter2, tail2, b2)
+  | NList (i1, j1, iter1, tail1, b1), NBinderList (i2, j2, iter2, tail2, b2) ->
+    (* They may overlap on a unique iteration of them *)
+    let vars1 = replace_var i1 j1 vars1 in
+    let vars2 = replace_var i2 j2 vars2 in
+    aux (vars1,vars2) renaming iter1 iter2;
+    aux vars renaming tail1 tail2
+  | t1, NList (i2, j2, iter2, tail2, b2)
+  | t1, NBinderList (i2, j2, iter2, tail2, b2) when lt ->
+    (* checking if t1 is a finite iteration of the pattern *)
+    let vars2 = replace_var i2 j2 vars2 in
+    aux (vars1,vars2) renaming t1 iter2;
+    let t1 = List.hd !tail in
+    tail := List.tl !tail;
+    (* either matching a new iteration, or matching the tail *)
+    (try aux vars renaming t1 tail2 with Exit -> aux vars renaming t1 t2)
+  | NList (i1, j1, iter1, tail1, b1), t2
+  | NBinderList (i1, j1, iter1, tail1, b1), t2 when lt ->
+    (* we see the NList as a single iteration *)
+    let vars1 = replace_var i1 j1 vars1 in
+    aux (vars1,vars2) renaming iter1 t2;
+    let t2 = match !tail with
+      | t::rest -> tail := rest; t
+      | _ -> (* ".." is in a discarded fine-grained position *) raise Exit in
+    (* it had to be a single iteration of iter1 *)
+    aux vars renaming tail1 t2
+  | NApp (t1, a1), NApp (t2, a2) -> aux vars renaming t1 t2; List.iter2 (aux vars renaming) a1 a2
+  | NLambda (na1, t1, u1), NLambda (na2, t2, u2)
+  | NProd (na1, t1, u1), NProd (na2, t2, u2) ->
+    aux vars renaming t1 t2;
+    let renaming = check_eq_name vars renaming na1 na2 in
+    aux vars renaming u1 u2
+  | NLetIn (na1, b1, t1, u1), NLetIn (na2, b2, t2, u2) ->
+    aux vars renaming b1 b2;
+    Option.iter2 (aux vars renaming) t1 t2;(* TODO : subtyping? *)
+    let renaming = check_eq_name vars renaming na1 na2 in
+    aux vars renaming u1 u2
+  | NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (* FIXME? *)
+    let check_pat (p1, t1) (p2, t2) =
+      if not (List.equal cases_pattern_eq p1 p2) then raise Exit; (* TODO: subtyping and renaming *)
+      aux vars renaming t1 t2
+    in
+    let eqf renaming (t1, (na1, o1)) (t2, (na2, o2)) =
+      aux vars renaming t1 t2;
+      let renaming = check_eq_name vars renaming na1 na2 in
+      let eq renaming (i1, n1) (i2, n2) =
+        if not (Ind.CanOrd.equal i1 i2) then raise Exit;
+        List.fold_left2 (check_eq_name vars) renaming n1 n2 in
+        Option.fold_left2 eq renaming o1 o2 in
+    let renaming = List.fold_left2 eqf renaming r1 r2 in
+    Option.iter2 (aux vars renaming) o1 o2;
+    List.iter2 check_pat p1 p2
+  | NLetTuple (nas1, (na1, o1), t1, u1), NLetTuple (nas2, (na2, o2), t2, u2) ->
+    aux vars renaming t1 t2;
+    let renaming = check_eq_name vars renaming na1 na2 in
+    Option.iter2 (aux vars renaming) o1 o2;
+    let renaming' = List.fold_left2 (check_eq_name vars) renaming nas1 nas2 in
+    aux vars renaming' u1 u2
+  | NIf (t1, (na1, o1), u1, r1), NIf (t2, (na2, o2), u2, r2) ->
+    aux vars renaming t1 t2;
+    aux vars renaming u1 u2;
+    aux vars renaming r1 r2;
+    let renaming = check_eq_name vars renaming na1 na2 in
+    Option.iter2 (aux vars renaming) o1 o2
+  | NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (* FIXME? *)
+    let eq renaming (na1, o1, t1) (na2, o2, t2) =
+      Option.iter2 (aux vars renaming) o1 o2;
+      aux vars renaming t1 t2;
+      check_eq_name vars renaming na1 na2
+    in
+    let renaming = Array.fold_left2 (fun r id1 id2 -> check_eq_id vars r id1 id2; (id1,id2)::r) renaming ids1 ids2 in
+    let renamings = Array.map2 (List.fold_left2 eq renaming) ts1 ts2 in
+    Array.iter3 (aux vars) renamings us1 us2;
+    Array.iter3 (aux vars) (Array.map ((@) renaming) renamings) rs1 rs2
+  | NSort s1, NSort s2 when glob_sort_eq s1 s2 -> ()
+  | NCast (t1, c1), NCast (t2, c2) ->
+    aux vars renaming t1 t2;
+    cast_type_iter2 (aux vars renaming) c1 c2
+  | NInt i1, NInt i2 when Uint63.equal i1 i2 -> ()
+  | NFloat f1, NFloat f2 when Float64.equal f1 f2 -> ()
+  | NArray(t1,def1,ty1), NArray(t2,def2,ty2) ->
+    Array.iter2 (aux vars renaming) t1 t2;
+    aux vars renaming def1 def2;
+    aux vars renaming ty1 ty2
+  | (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _
+    | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _
+    | NRec _ | NSort _ | NCast _ | NInt _ | NFloat _ | NArray _), _ -> raise Exit in
+  try
+    let _ = aux (vars1,vars2) [] t1 t2 in
+    if not lt then
+      (* Check that order of notation metavariables does not matter *)
+      List.iter2 check_alphameta vars1 vars2;
+    not lt || !strictly_lt
+  with Exit | (* Option.iter2: *) Option.Heterogeneous | Invalid_argument _ -> false
+
+let eq_notation_constr vars t1 t2 = t1 == t2 || compare_notation_constr false vars t1 t2
+
+let strictly_finer_notation_constr vars t1 t2 = compare_notation_constr true vars t1 t2
 
 (**********************************************************************)
 (* Re-interpret a notation as a glob_constr, taking care of binders   *)
@@ -154,8 +254,6 @@ let rec subst_glob_vars l gc = DAst.map (function
   | _ -> DAst.get (map_glob_constr (subst_glob_vars l) gc) (* assume: id is not binding *)
   ) gc
 
-let ldots_var = Id.of_string ".."
-
 type 'a binder_status_fun = {
   no : 'a -> 'a;
   restart_prod : 'a -> 'a;
@@ -749,12 +847,6 @@ let is_bindinglist_meta id metas =
 
 exception No_match
 
-let rec alpha_var id1 id2 = function
-  | (i1,i2)::_ when Id.equal i1 id1 -> Id.equal i2 id2
-  | (i1,i2)::_ when Id.equal i2 id2 -> Id.equal i1 id1
-  | _::idl -> alpha_var id1 id2 idl
-  | [] -> Id.equal id1 id2
-
 let alpha_rename alpmetas v =
   if alpmetas == [] then v
   else try rename_glob_vars alpmetas v with UnsoundRenaming -> raise No_match
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 3cc6f82ec8..3182ea96d7 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -16,6 +16,11 @@ open Glob_term
 
 val eq_notation_constr : Id.t list * Id.t list -> notation_constr -> notation_constr -> bool
 
+val strictly_finer_notation_constr : Id.t list * Id.t list -> notation_constr -> notation_constr -> bool
+(** Tell if [t1] is a strict refinement of [t2]
+    (this is a partial order and returning [false] does not mean that
+    [t2] is finer than [t1]) *)
+
 (** Substitution of kernel names in interpretation data                *)
 
 val subst_interpretation :
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 623ca316c9..a9bed49922 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -120,14 +120,14 @@ where
 letpair x [1] = {0};
 return (1, 2, 3, 4)
      : nat * nat * nat * nat
-{{ 1 | 1 // 1 }}
-     : nat
-!!! _ _ : nat, True
-     : (nat -> Prop) * ((nat -> Prop) * Prop)
 ((*1).2).3
      : nat
 *(1.2)
      : nat
+{{ 1 | 1 // 1 }}
+     : nat
+!!! _ _ : nat, True
+     : (nat -> Prop) * ((nat -> Prop) * Prop)
 ! '{{x, y}}, x.y = 0
      : Prop
 exists x : nat,
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index ce97d909a7..04a91c14d9 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -181,6 +181,13 @@ Notation "'letpair' x [1] = { a } ; 'return' ( b0 , b1 , .. , b2 )" :=
   (let x:=a in ( .. (b0,b1) .., b2)).
 Check letpair x [1] = {0}; return (1,2,3,4).
 
+(* Allow level for leftmost nonterminal when printing-only, BZ#5739 *)
+
+Notation "* x" := (id x) (only printing, at level 15, format "* x").
+Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y").
+Check (((id 1) + 2) + 3).
+Check (id (1 + 2)).
+
 (* Test spacing in #5569 *)
 
 Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut)
@@ -191,13 +198,6 @@ Check 1+1+1.
 Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder).
 Check !!! (x y:nat), True.
 
-(* Allow level for leftmost nonterminal when printing-only, BZ#5739 *)
-
-Notation "* x" := (id x) (only printing, at level 15, format "* x").
-Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y").
-Check (((id 1) + 2) + 3).
-Check (id (1 + 2)).
-
 (* Test contraction of "forall x, let 'pat := x in ..." into "forall 'pat, ..." *)
 (* for isolated "forall" (was not working already in 8.6) *)
 Notation "! x .. y , A" := (id (forall x, .. (id (forall y, A)) .. )) (at level 200, x binder).
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index a6fd39c29b..86c4b3cccc 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -179,3 +179,21 @@ Found an inductive type while a pattern was expected.
      : Prop
 !!!! (nat, id), nat = true /\ id = false
      : Prop
+∀ x : nat, x = 0
+     : Prop
+∀₁ x, x = 0
+     : Prop
+∀₁ x, x = 0
+     : Prop
+∀₂ x y, x + y = 0
+     : Prop
+((1, 2))
+     : nat * nat
+%% [x == 1]
+     : Prop
+%%% [1]
+     : Prop
+[[2]]
+     : nat * nat
+%%%
+     : Type
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 0731819bba..6af192ea82 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -414,3 +414,76 @@ Module P.
   End NotationBinderNotMixedWithTerms.
 
 End P.
+
+Module MorePrecise1.
+
+(* A notation with limited iteration is strictly more precise than a
+   notation with unlimited iteration *)
+
+Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
+  (at level 200, x binder, y binder, right associativity,
+  format "'[  ' '[  ' ∀  x  ..  y ']' ,  '/' P ']'") : type_scope.
+
+Check forall x, x = 0.
+
+Notation "∀₁ z , P" := (forall z, P)
+  (at level 200, right associativity) : type_scope.
+
+Check forall x, x = 0.
+
+Notation "∀₂ y x , P" := (forall y x, P)
+  (at level 200, right associativity) : type_scope.
+
+Check forall x, x = 0.
+Check forall x y, x + y = 0.
+
+Notation "(( x , y ))" := (x,y) : core_scope.
+
+Check ((1,2)).
+
+End MorePrecise1.
+
+Module MorePrecise2.
+
+(* Case of a bound binder *)
+Notation "%% [ x == y ]" := (forall x, S x = y) (at level 0, x pattern, y at level 60).
+
+(* Case of an internal binder *)
+Notation "%%% [ y ]" := (forall x : nat, x = y) (at level 0).
+
+(* Check that the two previous notations are indeed finer *)
+Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
+  (at level 200, x binder, y binder, right associativity,
+  format "'[  ' '[  ' ∀  x  ..  y ']' ,  '/' P ']'").
+Notation "∀' x .. y , P" := (forall y, .. (forall x, P) ..)
+  (at level 200, x binder, y binder, right associativity,
+  format "'[  ' '[  ' ∀'  x  ..  y ']' ,  '/' P ']'").
+
+Check %% [x == 1].
+Check %%% [1].
+
+Notation "[[ x ]]" := (pair 1 x).
+
+Notation "( x ; y ; .. ; z )" := (pair .. (pair x y) .. z).
+Notation "[ x ; y ; .. ; z ]" := (pair .. (pair x z) .. y).
+
+(* Check which is finer *)
+Check [[ 2 ]].
+
+End MorePrecise2.
+
+Module MorePrecise3.
+
+(* This is about a binder not bound in a notation being strictly more
+   precise than a binder bound in the notation (since the notation
+   applies - a priori - stricly less often) *)
+
+Notation "%%%" := (forall x, x) (at level 0).
+
+Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
+  (at level 200, x binder, y binder, right associativity,
+  format "'[  ' '[  ' ∀  x  ..  y ']' ,  '/' P ']'").
+
+Check %%%.
+
+End MorePrecise3.
diff --git a/test-suite/output/bug_10824.out b/test-suite/output/bug_10824.out
new file mode 100644
index 0000000000..4bc5aafbca
--- /dev/null
+++ b/test-suite/output/bug_10824.out
@@ -0,0 +1,4 @@
+!!
+     : Prop
+!!
+     : Prop
diff --git a/test-suite/output/bug_10824.v b/test-suite/output/bug_10824.v
new file mode 100644
index 0000000000..01271f7d61
--- /dev/null
+++ b/test-suite/output/bug_10824.v
@@ -0,0 +1,12 @@
+Module A.
+Notation F := False.
+Notation "!!" := False (at level 100).
+Check False.
+End A.
+
+Module B.
+Notation "!!" := False (at level 100).
+Notation F := False.
+Notation "!!" := False (at level 100).
+Check False.
+End B.
diff --git a/test-suite/output/bug_7443.out b/test-suite/output/bug_7443.out
new file mode 100644
index 0000000000..446ec6a1ad
--- /dev/null
+++ b/test-suite/output/bug_7443.out
@@ -0,0 +1,13 @@
+Literal 1
+     : Type
+[1]
+     : Type
+Literal 1
+     : Type
+[1]
+     : Type
+The command has indeed failed with message:
+The term "1" has type "Datatypes.nat" while it is expected to have type
+ "denote ?t".
+Literal 1
+     : Type
diff --git a/test-suite/output/bug_7443.v b/test-suite/output/bug_7443.v
new file mode 100644
index 0000000000..33f76dbcfa
--- /dev/null
+++ b/test-suite/output/bug_7443.v
@@ -0,0 +1,37 @@
+Inductive type := nat | bool.
+Definition denote (t : type)
+  := match t with
+     | nat => Datatypes.nat
+     | bool => Datatypes.bool
+     end.
+Ltac reify t :=
+  lazymatch eval cbv beta in t with
+  | Datatypes.nat => nat
+  | Datatypes.bool => bool
+  end.
+Notation reify t := (ltac:(let rt := reify t in exact rt)) (only parsing).
+Notation reify_type_of e := (reify ((fun t (_ : t) => t) _ e)) (only parsing).
+Axiom Literal : forall {t}, denote t -> Type.
+Declare Scope foo_scope.
+Delimit Scope foo_scope with foo.
+Open Scope foo_scope.
+Section A.
+  Notation "[ x ]" := (Literal (t:=reify_type_of x) x) (only parsing) : foo_scope.
+  Check [1]. (* Literal 1 : Type *) (* as expected *)
+  Notation "[ x ]" := (Literal x) : foo_scope.
+  Check @Literal nat 1. (* Incorred: gives Literal 1 : Type when it should give [1]. Fixed by #12950 *)
+  Notation "[ x ]" := (Literal (t:=reify_type_of x) x) (only parsing) : foo_scope.
+  Check [1]. (* Incorrect: gives Literal 1 : Type when it should give [1]. This is disputable:
+  #12950 considers that giving an only parsing a previous both-parsing-and-printing notation *)
+End A.
+Section B.
+  Notation "[ x ]" := (Literal x) : foo_scope.
+  Check @Literal nat 1. (* [1] : Type *)
+  Fail Check [1]. (* As expected: The command has indeed failed with message:
+  The term "1" has type "Datatypes.nat" while it is expected to have type
+   "denote ?t". *)
+  Notation "[ x ]" := (Literal (t:=reify_type_of x) x) (only parsing) : foo_scope.
+  Check [1]. (* Should succeed, but instead fails with: Error:
+  The term "1" has type "Datatypes.nat" while it is expected to have type
+  "denote ?t". Fixed by #12950, but previous declaration is cancelled by #12950. *)
+End B.