Merge PR #11142: Slightly improving strategy about when to print coercion or explicitly print implicit arguments

Ack-by: SkySkimmer
Reviewed-by: ejgallego

2 files changed, 15 insertions, 0 deletions

diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out
index 28afd06fbc..ef7667936c 100644
--- a/test-suite/output/Implicit.out
+++ b/test-suite/output/Implicit.out
@@ -12,3 +12,8 @@ map id' (1 :: nil)
      : list nat
 map (id'' (A:=nat)) (1 :: nil)
      : list nat
+fix f (x : nat) : option nat := match x with
+                                | 0 => None
+                                | S _ => x
+                                end
+     : nat -> option nat
diff --git a/test-suite/output/Implicit.v b/test-suite/output/Implicit.v
index 306532c0df..a7c4399e38 100644
--- a/test-suite/output/Implicit.v
+++ b/test-suite/output/Implicit.v
@@ -51,3 +51,13 @@ Definition id'' (A:Type) (x:A) := x.
 
 Check map (@id'' nat) (1::nil).
 
+Module MatchBranchesInContext.
+
+Set Implicit Arguments.
+Set Contextual Implicit.
+
+Inductive option A := None | Some (a:A).
+Coercion some_nat := @Some nat.
+Check fix f x := match x with 0 => None | n => some_nat n end.
+
+End MatchBranchesInContext.