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

Ack-by: SkySkimmer
Reviewed-by: ejgallego

1 files changed, 6 insertions, 4 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 0a3ee59f4e..828c88adbe 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -973,17 +973,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),
@@ -1006,7 +1008,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 ->
@@ -1017,7 +1019,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))