Revert "Isolating and exporting a function for printing body of a recursive definition."

This reverts commit 5598db7882f111b1fe3aa22936679e06b7a2f673.

1 files changed, 11 insertions, 10 deletions

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index efdaa366b..17926055e 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -381,14 +381,6 @@ module Make
     | None -> mt ()
     | Some pl -> str"@{" ++ prlist_with_sep spc pr_lident pl ++ str"}"
 
-  let pr_rec_definition ((((loc,id),pl),ro,bl,type_,def),ntn) =
-    let pr_pure_lconstr c = Flags.without_option Flags.beautify_file pr_lconstr c in
-    let annot = pr_guard_annot pr_lconstr_expr bl ro in
-    pr_id id ++ pr_univs pl ++ pr_binders_arg bl ++ annot
-    ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
-    ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr def) def
-    ++ prlist (pr_decl_notation pr_constr) ntn
-
   let pr_statement head (idpl,(bl,c,guard)) =
     assert (not (Option.is_empty idpl));
     let id, pl = Option.get idpl in
@@ -797,10 +789,19 @@ module Make
           | Some Local -> "Local "
           | None | Some Global -> ""
         in
+        let pr_pure_lconstr c =
+          Flags.without_option Flags.beautify_file pr_lconstr c in
+        let pr_onerec = function
+          | (((loc,id),pl),ro,bl,type_,def),ntn ->
+            let annot = pr_guard_annot pr_lconstr_expr bl ro in
+            pr_id id ++ pr_univs pl ++ pr_binders_arg bl ++ annot
+            ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
+            ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr def) def ++
+              prlist (pr_decl_notation pr_constr) ntn
+        in
         return (
           hov 0 (str local ++ keyword "Fixpoint" ++ spc () ++
-                   prlist_with_sep (fun _ -> fnl () ++ keyword "with"
-                     ++ spc ()) pr_rec_definition recs)
+                   prlist_with_sep (fun _ -> fnl () ++ keyword "with" ++ spc ()) pr_onerec recs)
         )
 
       | VernacCoFixpoint (local, corecs) ->