In printing patterns, distinguish the case of a notation to @id.

This is a case which conventionally deactivates implicit arguments.

1 files changed, 12 insertions, 9 deletions

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index d1eb50d370..59a58d643c 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -1364,35 +1364,37 @@ let match_cases_pattern_list match_fun metas sigma rest x y iter termin revert =
 
 let rec match_cases_pattern metas (terms,termlists,(),() as sigma) a1 a2 =
  match DAst.get a1, a2 with
-  | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(0,[])
-  | PatVar Anonymous, NHole _ -> sigma,(0,[])
+  | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(false,0,[])
+  | PatVar Anonymous, NHole _ -> sigma,(false,0,[])
   | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (GlobRef.ConstructRef r2) when eq_constructor r1 r2 ->
       let l = try add_patterns_for_params_remove_local_defs (Global.env ()) r1 largs with Not_found -> raise No_match in
-      sigma,(0,l)
+      sigma,(false,0,l)
   | PatCstr ((ind,_ as r1),args1,Anonymous), NApp (NRef (GlobRef.ConstructRef r2),l2)
       when eq_constructor r1 r2 ->
       let l1 = try add_patterns_for_params_remove_local_defs (Global.env()) r1 args1 with Not_found -> raise No_match in
       let le2 = List.length l2 in
-      if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length l1
+      if le2 > List.length l1
       then
         raise No_match
       else
         let l1',more_args = Util.List.chop le2 l1 in
-        (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args)
+        (* Convention: notations to @f don't keep implicit arguments *)
+        let no_implicit = le2 = 0 in
+        (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(no_implicit,le2,more_args)
   | r1, NList (x,y,iter,termin,revert) ->
       (match_cases_pattern_list (match_cases_pattern_no_more_args)
-        metas (terms,termlists,(),()) a1 x y iter termin revert),(0,[])
+        metas (terms,termlists,(),()) a1 x y iter termin revert),(false,0,[])
   | _ -> raise No_match
 
 and match_cases_pattern_no_more_args metas sigma a1 a2 =
     match match_cases_pattern metas sigma a1 a2 with
-      | out,(_,[]) -> out
+      | out,(_,_,[]) -> out
       | _ -> raise No_match
 
 let match_ind_pattern metas sigma ind pats a2 =
   match a2 with
   | NRef (GlobRef.IndRef r2) when eq_ind ind r2 ->
-      sigma,(0,pats)
+      sigma,(false,0,pats)
   | NApp (NRef (GlobRef.IndRef r2),l2)
       when eq_ind ind r2 ->
       let le2 = List.length l2 in
@@ -1401,7 +1403,8 @@ let match_ind_pattern metas sigma ind pats a2 =
         raise No_match
       else
         let l1',more_args = Util.List.chop le2 pats in
-        (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args)
+        let no_implicit = le2 = 0 in
+        (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(no_implicit,le2,more_args)
   |_ -> raise No_match
 
 let reorder_canonically_substitution terms termlists metas =