Small improvement to "fix"/"cofix" printing rule.

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.

gives:

fix f (x : nat) : option nat :=
  match x with
  | 0 => None (A:=nat)
  | S _ => some_nat x
  end

See discussion at
https://github.com/coq/coq/pull/11142/files/718c1422954794e0e33a87cf4c9111c00cc186dd#r377054717

2 files changed, 18 insertions, 20 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index b55a41471a..49c475dff4 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -384,12 +384,12 @@ let tag_var = tag Tag.variable
     if is_open then pr_delimited_binders pr_com_at sep pr_c
     else pr_undelimited_binders sep pr_c
 
-  let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c =
+  let pr_recursive_decl pr pr_dangling kw dangling_with_for id bl annot t c =
     let pr_body =
       if dangling_with_for then pr_dangling else pr in
-    pr_id id ++ (if bl = [] then mt () else str" ") ++
+    hov 0 (str kw ++ spc () ++ pr_id id ++ (if bl = [] then mt () else str" ") ++
       hov 0 (pr_undelimited_binders spc (pr ltop) bl ++ annot) ++
-      pr_opt_type_spc pr t ++ str " :=" ++
+      pr_opt_type_spc pr t ++ str " :=") ++
       pr_sep_com (fun () -> brk(1,2)) (pr_body ltop) c
 
   let pr_guard_annot pr_aux bl ro =
@@ -413,19 +413,19 @@ let tag_var = tag Tag.variable
             match id with None -> mt() | Some id -> spc () ++ pr_lident id ++
               (match r with None -> mt() | Some r -> str" on " ++ pr_aux r) ++ str"}"
 
-  let pr_fixdecl pr prd dangling_with_for ({v=id},ro,bl,t,c) =
+  let pr_fixdecl pr prd kw dangling_with_for ({v=id},ro,bl,t,c) =
     let annot = pr_guard_annot (pr lsimpleconstr) bl ro in
-    pr_recursive_decl pr prd dangling_with_for id bl annot t c
+    pr_recursive_decl pr prd kw dangling_with_for id bl annot t c
 
-  let pr_cofixdecl pr prd dangling_with_for ({v=id},bl,t,c) =
-    pr_recursive_decl pr prd dangling_with_for id bl (mt()) t c
+  let pr_cofixdecl pr prd kw dangling_with_for ({v=id},bl,t,c) =
+    pr_recursive_decl pr prd kw dangling_with_for id bl (mt()) t c
 
-  let pr_recursive pr_decl id = function
+  let pr_recursive kw pr_decl id = function
     | [] -> anomaly (Pp.str "(co)fixpoint with no definition.")
-    | [d1] -> pr_decl false d1
+    | [d1] -> pr_decl kw false d1
     | dl ->
-      prlist_with_sep (fun () -> fnl() ++ keyword "with" ++ spc ())
-        (pr_decl true) dl ++
+      prlist_with_sep (fun () -> fnl())
+        (pr_decl "with" true) dl ++
         fnl() ++ keyword "for" ++ spc () ++ pr_id id
 
   let pr_asin pr na indnalopt =
@@ -491,15 +491,13 @@ let tag_var = tag Tag.variable
         return (pr_cref r us, latom)
       | CFix (id,fix) ->
         return (
-          hov 0 (keyword "fix" ++ spc () ++
-                   pr_recursive
+          hv 0 (pr_recursive "fix"
                    (pr_fixdecl (pr mt) (pr_dangling_with_for mt pr)) id.v fix),
           lfix
         )
       | CCoFix (id,cofix) ->
         return (
-          hov 0 (keyword "cofix" ++ spc () ++
-                   pr_recursive
+          hv 0 (pr_recursive "cofix"
                    (pr_cofixdecl (pr mt) (pr_dangling_with_for mt pr)) id.v cofix),
           lfix
         )
diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out
index 6879cbc3c2..60bc9cbf55 100644
--- a/test-suite/output/Fixpoint.out
+++ b/test-suite/output/Fixpoint.out
@@ -1,8 +1,8 @@
-fix F (A B : Set) (f : A -> B) (l : list A) {struct l} : 
-list B := match l with
-          | nil => nil
-          | a :: l0 => f a :: F A B f l0
-          end
+fix F (A B : Set) (f : A -> B) (l : list A) {struct l} : list B :=
+  match l with
+  | nil => nil
+  | a :: l0 => f a :: F A B f l0
+  end
      : forall A B : Set, (A -> B) -> list A -> list B
 let fix f (m : nat) : nat := match m with
                              | 0 => 0