From fd40254f02f4640bbfcad5a010a8a0062989eeb9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 18 Nov 2019 15:29:18 +0100
Subject: Mini-improvements in when to skip coercions or explicitly print
 implicit args.

If a return type is given to a match/if/let, then we are in context
(and thus may skip coercions or not make explicit those implicit
arguments inferable from context). Note that the notion of "inferable
from context" remains anyway an approximation in the case of implicit
arguments.

The body of a fix/cofix is also in context.

Also fixed an inconsistency with parsing in the scope used to print
the body of a fix.
---
 test-suite/output/Implicit.out |  5 +++++
 test-suite/output/Implicit.v   | 10 ++++++++++
 2 files changed, 15 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out
index 5f22eb5d7c..d081089652 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.
-- 
cgit v1.2.3