diff options
| author | Guillaume Melquiond | 2021-01-13 18:29:11 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2021-01-13 21:03:41 +0100 |
| commit | e881720a724ffa4e6201cc1d460c66ce373713d9 (patch) | |
| tree | e9e70f031996d23609f5d8ef5fd1b381646189fd /vernac | |
| parent | 9fef12aadf0e7afea3d89a00cb7216b2b008cf5c (diff) | |
Make sure "Print Module" write a dot at the end of inductive definitions.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/printmod.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/printmod.ml b/vernac/printmod.ml index fdf7f6c74a..ba4a7857e7 100644 --- a/vernac/printmod.ml +++ b/vernac/printmod.ml @@ -124,7 +124,7 @@ let print_mutual_inductive env mind mib udecl = let sigma = Evd.from_ctx (UState.of_binders bl) in hov 0 (def keyword ++ spc () ++ prlist_with_sep (fun () -> fnl () ++ str" with ") - (print_one_inductive env sigma mib) inds ++ + (print_one_inductive env sigma mib) inds ++ str "." ++ Printer.pr_universes sigma ?variance:mib.mind_variance mib.mind_universes) let get_fields = @@ -173,7 +173,7 @@ let print_record env mind mib udecl = prlist_with_sep (fun () -> str ";" ++ brk(2,0)) (fun (id,b,c) -> Id.print id ++ str (if b then " : " else " := ") ++ - Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++ + Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }." ++ Printer.pr_universes sigma ?variance:mib.mind_variance mib.mind_universes ) |