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.

3 files changed, 21 insertions, 4 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index c198c4eb9b..35fa32dc69 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -969,17 +969,19 @@ let rec extern inctx scopes vars r =
                              ) x))
                 tml
     in
-    let eqns = List.map (extern_eqn inctx scopes vars) (factorize_eqns eqns) in
+    let eqns = List.map (extern_eqn (inctx || rtntypopt <> None) scopes vars) (factorize_eqns eqns) in
     CCases (sty,rtntypopt',tml,eqns)
 
   | GLetTuple (nal,(na,typopt),tm,b) ->
-    CLetTuple (List.map CAst.make nal,
+      let inctx = inctx || typopt <> None in
+      CLetTuple (List.map CAst.make nal,
         (Option.map (fun _ -> (make na)) typopt,
          Option.map (extern_typ scopes (add_vname vars na)) typopt),
         sub_extern false scopes vars tm,
         extern inctx scopes (List.fold_left add_vname vars nal) b)
 
   | GIf (c,(na,typopt),b1,b2) ->
+      let inctx = inctx || typopt <> None in
       CIf (sub_extern false scopes vars c,
         (Option.map (fun _ -> (CAst.make na)) typopt,
          Option.map (extern_typ scopes (add_vname vars na)) typopt),
@@ -1002,7 +1004,7 @@ let rec extern inctx scopes vars r =
                    | Some x -> Some (CAst.make @@ CStructRec (CAst.make @@ Name.get_id (List.nth assums x)))
                              in
                  ((CAst.make fi), n, bl, extern_typ scopes vars0 ty,
-                  extern false scopes vars1 def)) idv
+                  sub_extern true scopes vars1 def)) idv
              in
              CFix (CAst.(make ?loc idv.(n)), Array.to_list listdecl)
          | GCoFix n ->
@@ -1013,7 +1015,7 @@ let rec extern inctx scopes vars r =
                  let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in
                  let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in
                  ((CAst.make fi),bl,extern_typ scopes vars0 tyv.(i),
-                  sub_extern false scopes vars1 bv.(i))) idv
+                  sub_extern true scopes vars1 bv.(i))) idv
              in
              CCoFix (CAst.(make ?loc idv.(n)),Array.to_list listdecl))
 
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.