diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-13 21:21:57 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-16 17:43:28 +0200 |
| commit | 334c8daf6569f36290a002597d8ff6dac4fb643f (patch) | |
| tree | 10dc120a701d19173058c2dbfc47df6b7a41ea6d /printing | |
| parent | 539990585352e89b3bfe426bed6ebbbaecb41d54 (diff) | |
Isolating and exporting a function for printing body of a recursive definition.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 21 | ||||
| -rw-r--r-- | printing/ppvernacsig.mli | 3 |
2 files changed, 13 insertions, 11 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 4b331ab8a..f3558054b 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -377,6 +377,14 @@ 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 @@ -785,19 +793,10 @@ 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_onerec recs) + prlist_with_sep (fun _ -> fnl () ++ keyword "with" + ++ spc ()) pr_rec_definition recs) ) | VernacCoFixpoint (local, corecs) -> diff --git a/printing/ppvernacsig.mli b/printing/ppvernacsig.mli index 5d1c89332..5e5e4bcf4 100644 --- a/printing/ppvernacsig.mli +++ b/printing/ppvernacsig.mli @@ -8,6 +8,9 @@ module type Pp = sig + (** Prints a fixpoint body *) + val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.std_ppcmds + (** Prints a vernac expression *) val pr_vernac_body : Vernacexpr.vernac_expr -> Pp.std_ppcmds |