From ab5454d3c2967b0baac1d98590c04a42651db132 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Wed, 18 Oct 2023 10:41:05 +0200
Subject: [PATCH] Fixes #18163: take implicit-printing mode into account for
 patterns.

---
 interp/constrextern.ml           | 12 ++++++++++--
 test-suite/output/PrintMatch.out | 16 ++++++++++++++++
 test-suite/output/PrintMatch.v   | 15 +++++++++++++++
 3 files changed, 41 insertions(+), 2 deletions(-)

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index b23ca10a12892..b13cd76f3f4d4 100644
--- a/interp/constrextern.ml
+++ b/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
diff --git a/test-suite/output/PrintMatch.out b/test-suite/output/PrintMatch.out
index 1fd70d937ee34..0e27ab40b4b62 100644
--- a/test-suite/output/PrintMatch.out
+++ b/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] _
diff --git a/test-suite/output/PrintMatch.v b/test-suite/output/PrintMatch.v
index df78c488eb41f..c9d2f1adfc802 100644
--- a/test-suite/output/PrintMatch.v
+++ b/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.