Fixes coq#18163: take implicit-printing mode into account for patterns.

interp/constrextern.ml

@@ -258,17 +258,25 @@ let drop_implicits_in_patt cst nb_expl args =
     | h::_, _ when is_status_implicit h -> None
     | _::t, hh::tt -> impls_fit (hh::l) (t,tt)
   in
+  let try_impls_fit (imps,args) =
+    if not !Constrintern.parsing_explicit &&
+       ((!Flags.raw_print || !print_implicits) &&
+        List.exists is_status_implicit imps)
+       (* Note: !print_implicits_explicit_args=true not supported for patterns *)
+    then None
+    else impls_fit [] (imps,args)
+  in
   let rec select = function
     | [] -> None
     | (_,imps)::imps_list ->
-      match impls_fit [] (imps,args) with
+      match try_impls_fit (imps,args) with
         | None -> select imps_list
         | x -> x
   in
   if Int.equal nb_expl 0 then select impl_data
   else
     let imps = List.skipn_at_least nb_expl (select_stronger_impargs impl_st) in
-    impls_fit [] (imps,args)
+    try_impls_fit (imps,args)
 
 let destPrim = function { CAst.v = CPrim t } -> Some t | _ -> None
 let destPatPrim = function { CAst.v = CPatPrim t } -> Some t | _ -> None

test-suite/output/PrintMatch.out

@@ -22,3 +22,19 @@ end
        P a (srefl a) -> forall (a0 : A) (s : seq a a0), P a0 s
 
 Arguments seq_rect A%type_scope a P%function_scope f a0 s
+eq_sym =
+fun (A : Type) (x y : A) (H : @eq A x y) =>
+match H in (@eq _ _ a) return (@eq A a x) with
+| @eq_refl _ _ => @eq_refl A x
+end
+     : forall (A : Type) (x y : A) (_ : @eq A x y), @eq A y x
+
+Arguments eq_sym [A]%type_scope [x y] _
+eq_sym =
+fun (A : Type) (x y : A) (H : x = y) =>
+match H in (_ = a) return (a = x) with
+| @eq_refl _ _ => @eq_refl A x
+end
+     : forall (A : Type) (x y : A), x = y -> y = x
+
+Arguments eq_sym [A]%type_scope [x y] _

test-suite/output/PrintMatch.v

@@ -1,5 +1,7 @@
 (* NB feel free to add other tests about printing match, not just about Match All Subterms *)
 
+Module MatchAllSubterms.
+
 Set Printing Match All Subterms.
 Set Printing Universes.
 
@@ -9,3 +11,16 @@ Print eqT_rect.
 Set Definitional UIP.
 Inductive seq {A} (a:A) : A -> SProp := srefl : seq a a.
 Print seq_rect.
+
+End MatchAllSubterms.
+
+Module Bug18163.
+
+Set Printing All.
+Print eq_sym.
+Unset Printing All.
+
+Set Printing Implicit.
+Print eq_sym.
+
+End Bug18163.