diff options
Diffstat (limited to 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index f9f4d7f7f8..c417ef8a66 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -427,7 +427,7 @@ let locate_modtype qid = let all = Nametab.locate_extended_all_modtype qid in let map mp = ModuleType mp, Nametab.shortest_qualid_of_modtype mp in let modtypes = List.map map all in - (** Don't forget the opened module types: they are not part of the same name tab. *) + (* Don't forget the opened module types: they are not part of the same name tab. *) let all = Nametab.locate_extended_all_dir qid in let map dir = let open Nametab.GlobDirRef in match dir with | DirOpenModtype _ -> Some (Dir dir, qid) @@ -575,7 +575,7 @@ let print_constant with_values sep sp udecl = in let env = Global.env () and sigma = Evd.from_ctx ctx in let pr_ltype = pr_ltype_env env sigma in - hov 0 (pr_polymorphic (Declareops.constant_is_polymorphic cb) ++ + hov 0 ( match val_0 with | None -> str"*** [ " ++ |