Merge PR #12683: Fixes #12682: printing bug with recursive notations for n-ary applications used with applied references

Reviewed-by: ejgallego

3 files changed, 30 insertions, 11 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 95df626d4c..3667757a2f 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -858,10 +858,17 @@ let extern_possible_prim_token (custom,scopes) r =
       insert_entry_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key)
 
 let filter_enough_applied nargs l =
+  (* This is to ensure that notations for coercions are used only when
+     the coercion is fully applied; not explicitly done yet, but we
+     could also expect that the notation is exactly talking about the
+     coercion *)
   match nargs with
   | None -> l
   | Some nargs ->
-  List.filter (fun (keyrule,pat,n as _rule) -> match n with Some n -> n > nargs | None -> false) l
+  List.filter (fun (keyrule,pat,n as _rule) ->
+      match n with
+      | AppBoundedNotation n -> n > nargs
+      | AppUnboundedNotation | NotAppNotation -> false) l
 
 (* Helper function for safe and optimal printing of primitive tokens  *)
 (* such as those for Int63                                            *)
@@ -1247,7 +1254,7 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
             [], [] in
         (* Adjust to the number of arguments expected by the notation *)
         let (t,args,argsscopes,argsimpls) = match n with
-          | Some n when nallargs >= n ->
+          | AppBoundedNotation n when nallargs >= n ->
               let args1, args2 = List.chop n args in
               let args2scopes = try List.skipn n argsscopes with Failure _ -> [] in
               let args2impls =
@@ -1257,12 +1264,13 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
                   []
                 else try List.skipn n argsimpls with Failure _ -> [] in
               DAst.make @@ GApp (f,args1), args2, args2scopes, args2impls
-          | None ->
+          | AppUnboundedNotation -> t, [], [], []
+          | NotAppNotation ->
             begin match DAst.get f with
             | GRef (ref,us) -> f, args, argsscopes, argsimpls
             | _ -> t, [], [], []
             end
-          | _ -> raise No_match in
+          | AppBoundedNotation _ -> raise No_match in
         (* Try matching ... *)
         let terms,termlists,binders,binderlists =
           match_notation_constr !print_universes t pat in
diff --git a/interp/notation.ml b/interp/notation.ml
index e282d62396..c4e9496b95 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -293,7 +293,12 @@ let key_compare k1 k2 = match k1, k2 with
 module KeyOrd = struct type t = key let compare = key_compare end
 module KeyMap = Map.Make(KeyOrd)
 
-type notation_rule = interp_rule * interpretation * int option
+type notation_applicative_status =
+  | AppBoundedNotation of int
+  | AppUnboundedNotation
+  | NotAppNotation
+
+type notation_rule = interp_rule * interpretation * notation_applicative_status
 
 let keymap_add key interp map =
   let old = try KeyMap.find key map with Not_found -> [] in
@@ -329,13 +334,14 @@ let cases_pattern_key c = match DAst.get c with
   | _ -> Oth
 
 let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
-  | NApp (NRef ref,args) -> RefKey(canonical_gr ref), Some (List.length args)
+  | NApp (NRef ref,args) -> RefKey(canonical_gr ref), AppBoundedNotation (List.length args)
   | NList (_,_,NApp (NRef ref,args),_,_)
   | NBinderList (_,_,NApp (NRef ref,args),_,_) ->
-      RefKey (canonical_gr ref), Some (List.length args)
-  | NRef ref -> RefKey(canonical_gr ref), None
-  | NApp (_,args) -> Oth, Some (List.length args)
-  | _ -> Oth, None
+      RefKey (canonical_gr ref), AppBoundedNotation (List.length args)
+  | NRef ref -> RefKey(canonical_gr ref), NotAppNotation
+  | NApp (_,args) -> Oth, AppBoundedNotation (List.length args)
+  | NList (_,_,NApp (NVar x,_),_,_) when x = Notation_ops.ldots_var -> Oth, AppUnboundedNotation
+  | _ -> Oth, NotAppNotation
 
 (** Dealing with precedences *)
 
diff --git a/interp/notation.mli b/interp/notation.mli
index c39bfa6e28..05ddd25a62 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -239,7 +239,12 @@ val declare_uninterpretation : interp_rule -> interpretation -> unit
 val interp_notation : ?loc:Loc.t -> notation -> subscopes ->
       interpretation * (notation_location * scope_name option)
 
-type notation_rule = interp_rule * interpretation * int option
+type notation_applicative_status =
+  | AppBoundedNotation of int
+  | AppUnboundedNotation
+  | NotAppNotation
+
+type notation_rule = interp_rule * interpretation * notation_applicative_status
 
 (** Return the possible notations for a given term *)
 val uninterp_notations : 'a glob_constr_g -> notation_rule list