Move prettyp (Print implementation) to vernac/

3 files changed, 1114 insertions, 0 deletions

diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
new file mode 100644
index 0000000000..fa534a0936
--- /dev/null
+++ b/vernac/prettyp.ml
@@ -0,0 +1,984 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* Changed by (and thus parts copyright ©) by Lionel Elie Mamane <lionel@mamane.lu>
+ * on May-June 2006 for implementation of abstraction of pretty-printing of objects.
+ *)
+
+open Pp
+open CErrors
+open Util
+open CAst
+open Names
+open Nameops
+open Termops
+open Declarations
+open Environ
+open Impargs
+open Libobject
+open Libnames
+open Globnames
+open Recordops
+open Printer
+open Printmod
+open Context.Rel.Declaration
+
+(* module RelDecl = Context.Rel.Declaration *)
+module NamedDecl = Context.Named.Declaration
+
+type object_pr = {
+  print_inductive           : MutInd.t -> UnivNames.univ_name_list option -> Pp.t;
+  print_constant_with_infos : Opaqueproof.indirect_accessor -> Constant.t -> UnivNames.univ_name_list option -> Pp.t;
+  print_section_variable    : env -> Evd.evar_map -> variable -> Pp.t;
+  print_syntactic_def       : env -> KerName.t -> Pp.t;
+  print_module              : mod_ops:Printmod.mod_ops -> bool -> ModPath.t -> Pp.t;
+  print_modtype             : mod_ops:Printmod.mod_ops -> ModPath.t -> Pp.t;
+  print_named_decl          : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t;
+  print_library_entry       : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option;
+  print_context             : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t;
+  print_typed_value_in_env  : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t;
+  print_eval                : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t;
+}
+
+let gallina_print_module  = print_module
+let gallina_print_modtype = print_modtype
+
+(**************)
+(** Utilities *)
+
+let print_closed_sections = ref false
+
+let pr_infos_list l = v 0 (prlist_with_sep cut (fun x -> x) l)
+
+let with_line_skip l = if List.is_empty l then mt() else fnl() ++ fnl () ++ pr_infos_list l
+
+let blankline = mt() (* add a blank sentence in the list of infos *)
+
+let add_colon prefix = if ismt prefix then mt () else prefix ++ str ": "
+
+let int_or_no n = if Int.equal n 0 then str "no" else int n
+
+(*******************)
+(** Basic printing *)
+
+let print_basename sp = pr_global (GlobRef.ConstRef sp)
+
+let print_ref reduce ref udecl =
+  let env = Global.env () in
+  let typ, univs = Typeops.type_of_global_in_context env ref in
+  let inst = Univ.make_abstract_instance univs in
+  let bl = UnivNames.universe_binders_with_opt_names (Environ.universes_of_global env ref) udecl in
+  let sigma = Evd.from_ctx (UState.of_binders bl) in
+  let typ = EConstr.of_constr typ in
+  let typ =
+    if reduce then
+      let ctx,ccl = Reductionops.splay_prod_assum env sigma typ
+      in EConstr.it_mkProd_or_LetIn ccl ctx
+    else typ in
+  let variance = let open GlobRef in match ref with
+    | VarRef _ | ConstRef _ -> None
+    | IndRef (ind,_) | ConstructRef ((ind,_),_) ->
+      let mind = Environ.lookup_mind ind env in
+      mind.Declarations.mind_variance
+  in
+  let inst =
+    if Global.is_polymorphic ref
+    then Printer.pr_universe_instance sigma inst
+    else mt ()
+  in
+  let priv = None in (* We deliberately don't print private univs in About. *)
+  hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++
+         Printer.pr_abstract_universe_ctx sigma ?variance univs ?priv)
+
+(********************************)
+(** Printing implicit arguments *)
+
+let pr_impl_name imp = Id.print (name_of_implicit imp)
+
+let print_impargs_by_name max = function
+  | []  -> []
+  | impls ->
+     let n = List.length impls in
+     [hov 0 (str (String.plural n "Argument") ++ spc() ++
+      prlist_with_sep pr_comma pr_impl_name impls ++ spc() ++
+      str (String.conjugate_verb_to_be n) ++ str" implicit" ++
+      (if max then strbrk " and maximally inserted" else mt()))]
+
+let print_one_impargs_list l =
+  let imps = List.filter is_status_implicit l in
+  let maximps = List.filter Impargs.maximal_insertion_of imps in
+  let nonmaximps = List.subtract (=) imps maximps in (* FIXME *)
+  print_impargs_by_name false nonmaximps @
+  print_impargs_by_name true maximps
+
+let print_impargs_list prefix l =
+  let l = extract_impargs_data l in
+  List.flatten (List.map (fun (cond,imps) ->
+    match cond with
+    | None ->
+        List.map (fun pp -> add_colon prefix ++ pp)
+          (print_one_impargs_list imps)
+    | Some (n1,n2) ->
+       [v 2 (prlist_with_sep cut (fun x -> x)
+         [(if ismt prefix then str "When" else prefix ++ str ", when") ++
+           str " applied to " ++
+           (if Int.equal n1 n2 then int_or_no n2 else
+            if Int.equal n1 0 then str "no more than " ++ int n2
+            else int n1 ++ str " to " ++ int_or_no n2) ++
+            str (String.plural n2 " argument") ++ str ":";
+          v 0 (prlist_with_sep cut (fun x -> x)
+            (if List.exists is_status_implicit imps
+            then print_one_impargs_list imps
+            else [str "No implicit arguments"]))])]) l)
+
+let print_renames_list prefix l =
+  if List.is_empty l then [] else
+  [add_colon prefix ++ str "Arguments are renamed to " ++
+    hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map Name.print l))]
+
+let need_expansion impl ref =
+  let typ, _ = Typeops.type_of_global_in_context (Global.env ()) ref in
+  let ctx = Term.prod_assum typ in
+  let nprods = List.count is_local_assum ctx in
+  not (List.is_empty impl) && List.length impl >= nprods &&
+    let _,lastimpl = List.chop nprods impl in
+      List.exists is_status_implicit lastimpl
+
+let print_impargs ref =
+  let ref = Smartlocate.smart_global ref in
+  let impl = implicits_of_global ref in
+  let has_impl = not (List.is_empty impl) in
+  (* Need to reduce since implicits are computed with products flattened *)
+  pr_infos_list
+    ([ print_ref (need_expansion (select_impargs_size 0 impl) ref) ref None;
+       blankline ] @
+    (if has_impl then print_impargs_list (mt()) impl
+     else [str "No implicit arguments"]))
+
+(*********************)
+(** Printing Scopes  *)
+
+let print_argument_scopes prefix = function
+  | [Some sc] ->
+      [add_colon prefix ++ str"Argument scope is [" ++ str sc ++ str"]"]
+  | l when not (List.for_all Option.is_empty l) ->
+     [add_colon prefix ++ hov 2 (str"Argument scopes are" ++ spc() ++
+      str "[" ++
+      pr_sequence (function Some sc -> str sc | None -> str "_") l ++
+      str "]")]
+  | _  -> []
+
+(*********************)
+(** Printing Opacity *)
+
+type opacity =
+  | FullyOpaque
+  | TransparentMaybeOpacified of Conv_oracle.level
+
+let opacity env =
+  function
+  | GlobRef.VarRef v when NamedDecl.is_local_def (Environ.lookup_named v env) ->
+      Some(TransparentMaybeOpacified
+        (Conv_oracle.get_strategy (Environ.oracle env) (VarKey v)))
+  | GlobRef.ConstRef cst ->
+      let cb = Environ.lookup_constant cst env in
+      (match cb.const_body with
+        | Undef _ | Primitive _ -> None
+        | OpaqueDef _ -> Some FullyOpaque
+        | Def _ -> Some
+          (TransparentMaybeOpacified
+            (Conv_oracle.get_strategy (Environ.oracle env) (ConstKey cst))))
+  | _ -> None
+
+let print_opacity ref =
+  match opacity (Global.env()) ref with
+    | None -> []
+    | Some s ->
+       [pr_global ref ++ str " is " ++
+        match s with
+          | FullyOpaque -> str "opaque"
+          | TransparentMaybeOpacified Conv_oracle.Opaque ->
+              str "basically transparent but considered opaque for reduction"
+          | TransparentMaybeOpacified lev when Conv_oracle.is_transparent lev ->
+              str "transparent"
+          | TransparentMaybeOpacified (Conv_oracle.Level n) ->
+              str "transparent (with expansion weight " ++ int n ++ str ")"
+          | TransparentMaybeOpacified Conv_oracle.Expand ->
+              str "transparent (with minimal expansion weight)"]
+
+(*******************)
+
+let print_if_is_coercion ref =
+  if Classops.coercion_exists ref then [pr_global ref ++ str " is a coercion"] else []
+
+(*******************)
+(* *)
+
+let pr_template_variables = function
+  | [] -> mt ()
+  | vars -> str "on " ++ prlist_with_sep spc UnivNames.pr_with_global_universes vars
+
+let print_polymorphism ref =
+  let poly = Global.is_polymorphic ref in
+  let template_poly = Global.is_template_polymorphic ref in
+  let template_checked = Global.is_template_checked ref in
+  let template_variables = Global.get_template_polymorphic_variables ref in
+  [ pr_global ref ++ str " is " ++
+      (if poly then str "universe polymorphic"
+       else if template_poly then
+         (if not template_checked then str "assumed " else mt()) ++
+         str "template universe polymorphic "
+         ++ h 0 (pr_template_variables template_variables)
+       else str "not universe polymorphic") ]
+
+let print_type_in_type ref =
+  let unsafe = Global.is_type_in_type ref in
+  if unsafe then
+    [ pr_global ref ++ str " relies on an unsafe universe hierarchy"]
+  else []
+
+let print_primitive_record recflag mipv = function
+  | PrimRecord _ ->
+    let eta = match recflag with
+    | CoFinite | Finite -> str" without eta conversion"
+    | BiFinite -> str " with eta conversion"
+    in
+    [Id.print mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."]
+  | FakeRecord | NotRecord -> []
+
+let print_primitive ref =
+  match ref with
+  | GlobRef.IndRef ind ->
+    let mib,_ = Global.lookup_inductive ind in
+      print_primitive_record mib.mind_finite mib.mind_packets mib.mind_record
+  | _ -> []
+
+let print_name_infos ref =
+  let impls = implicits_of_global ref in
+  let scopes = Notation.find_arguments_scope ref in
+  let renames =
+    try Arguments_renaming.arguments_names ref with Not_found -> [] in
+  let type_info_for_implicit =
+    if need_expansion (select_impargs_size 0 impls) ref then
+      (* Need to reduce since implicits are computed with products flattened *)
+      [str "Expanded type for implicit arguments";
+       print_ref true ref None; blankline]
+    else
+      [] in
+  print_type_in_type ref @
+  print_primitive ref @
+  type_info_for_implicit @
+  print_renames_list (mt()) renames @
+  print_impargs_list (mt()) impls @
+  print_argument_scopes (mt()) scopes @
+  print_if_is_coercion ref
+
+let print_id_args_data test pr id l =
+  if List.exists test l then
+    pr (str "For " ++ Id.print id) l
+  else
+    []
+
+let print_args_data_of_inductive_ids get test pr sp mipv =
+  List.flatten (Array.to_list (Array.mapi
+    (fun i mip ->
+      print_id_args_data test pr mip.mind_typename (get (GlobRef.IndRef (sp,i))) @
+      List.flatten (Array.to_list (Array.mapi
+        (fun j idc ->
+          print_id_args_data test pr idc (get (GlobRef.ConstructRef ((sp,i),j+1))))
+        mip.mind_consnames)))
+    mipv))
+
+let print_inductive_implicit_args =
+  print_args_data_of_inductive_ids
+    implicits_of_global (fun l -> not (List.is_empty (positions_of_implicits l)))
+    print_impargs_list
+
+let print_inductive_renames =
+  print_args_data_of_inductive_ids
+    (fun r ->
+      try Arguments_renaming.arguments_names r with Not_found -> [])
+    ((!=) Anonymous)
+    print_renames_list
+
+let print_inductive_argument_scopes =
+  print_args_data_of_inductive_ids
+    Notation.find_arguments_scope (Option.has_some) print_argument_scopes
+
+let print_bidi_hints gr =
+  match Pretyping.get_bidirectionality_hint gr with
+  | None -> []
+  | Some nargs ->
+    [str "Using typing information from context after typing the " ++ int nargs ++ str " first arguments"]
+
+(*********************)
+(* "Locate" commands *)
+
+type 'a locatable_info = {
+  locate : qualid -> 'a option;
+  locate_all : qualid -> 'a list;
+  shortest_qualid : 'a -> qualid;
+  name : 'a -> Pp.t;
+  print : 'a -> Pp.t;
+  about : 'a -> Pp.t;
+}
+
+type locatable = Locatable : 'a locatable_info -> locatable
+
+type logical_name =
+  | Term of GlobRef.t
+  | Dir of Nametab.GlobDirRef.t
+  | Syntactic of KerName.t
+  | ModuleType of ModPath.t
+  | Other : 'a * 'a locatable_info -> logical_name
+  | Undefined of qualid
+
+(** Generic table for objects that are accessible through a name. *)
+let locatable_map : locatable String.Map.t ref = ref String.Map.empty
+
+let register_locatable name f =
+  locatable_map := String.Map.add name (Locatable f) !locatable_map
+
+exception ObjFound of logical_name
+
+let locate_any_name qid =
+  try Term (Nametab.locate qid)
+  with Not_found ->
+  try Syntactic (Nametab.locate_syndef qid)
+  with Not_found ->
+  try Dir (Nametab.locate_dir qid)
+  with Not_found ->
+  try ModuleType (Nametab.locate_modtype qid)
+  with Not_found ->
+    let iter _ (Locatable info) = match info.locate qid with
+    | None -> ()
+    | Some ans -> raise (ObjFound (Other (ans, info)))
+    in
+    try String.Map.iter iter !locatable_map; Undefined qid
+    with ObjFound obj -> obj
+
+let pr_located_qualid = function
+  | Term ref ->
+      let ref_str = let open GlobRef in match ref with
+          ConstRef _ -> "Constant"
+        | IndRef _ -> "Inductive"
+        | ConstructRef _ -> "Constructor"
+        | VarRef _ -> "Variable" in
+      str ref_str ++ spc () ++ pr_path (Nametab.path_of_global ref)
+  | Syntactic kn ->
+      str "Notation" ++ spc () ++ pr_path (Nametab.path_of_syndef kn)
+  | Dir dir ->
+      let s,dir =
+        let open Nametab in
+        let open GlobDirRef in match dir with
+        | DirOpenModule { obj_dir ; _ } -> "Open Module", obj_dir
+        | DirOpenModtype { obj_dir ; _ } -> "Open Module Type", obj_dir
+        | DirOpenSection { obj_dir ; _ } -> "Open Section", obj_dir
+        | DirModule { obj_dir ; _ } -> "Module", obj_dir
+      in
+      str s ++ spc () ++ DirPath.print dir
+  | ModuleType mp ->
+      str "Module Type" ++ spc () ++ pr_path (Nametab.path_of_modtype mp)
+  | Other (obj, info) -> info.name obj
+  | Undefined qid ->
+      pr_qualid qid ++ spc () ++ str "not a defined object."
+
+let canonize_ref = let open GlobRef in function
+  | ConstRef c ->
+    let kn = Constant.canonical c in
+    if KerName.equal (Constant.user c) kn then None
+    else Some (ConstRef (Constant.make1 kn))
+  | IndRef (ind,i) ->
+    let kn = MutInd.canonical ind in
+    if KerName.equal (MutInd.user ind) kn then None
+    else Some (IndRef (MutInd.make1 kn, i))
+  | ConstructRef ((ind,i),j) ->
+    let kn = MutInd.canonical ind in
+    if KerName.equal (MutInd.user ind) kn then None
+    else Some (ConstructRef ((MutInd.make1 kn, i),j))
+  | VarRef _ -> None
+
+let display_alias = function
+  | Term r ->
+    begin match canonize_ref r with
+    | None -> mt ()
+    | Some r' ->
+      let q' = Nametab.shortest_qualid_of_global Id.Set.empty r' in
+      spc () ++ str "(alias of " ++ pr_qualid q' ++ str ")"
+    end
+  | _ -> mt ()
+
+let locate_term qid =
+  let expand = function
+    | TrueGlobal ref ->
+        Term ref, Nametab.shortest_qualid_of_global Id.Set.empty ref
+    | SynDef kn ->
+        Syntactic kn, Nametab.shortest_qualid_of_syndef Id.Set.empty kn
+  in
+  List.map expand (Nametab.locate_extended_all qid)
+
+let locate_module qid =
+  let all = Nametab.locate_extended_all_dir qid in
+  let map dir = let open Nametab.GlobDirRef in match dir with
+  | DirModule { Nametab.obj_mp ; _ } -> Some (Dir dir, Nametab.shortest_qualid_of_module obj_mp)
+  | DirOpenModule _ -> Some (Dir dir, qid)
+  | _ -> None
+  in
+  List.map_filter map all
+
+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. *)
+  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)
+  | _ -> None
+  in
+  modtypes @ List.map_filter map all
+
+let locate_other s qid =
+  let Locatable info = String.Map.find s !locatable_map in
+  let ans = info.locate_all qid in
+  let map obj = (Other (obj, info), info.shortest_qualid obj) in
+  List.map map ans
+
+type locatable_kind =
+| LocTerm
+| LocModule
+| LocOther of string
+| LocAny
+
+let print_located_qualid name flags qid =
+  let located = match flags with
+  | LocTerm -> locate_term qid
+  | LocModule -> locate_modtype qid @ locate_module qid
+  | LocOther s -> locate_other s qid
+  | LocAny ->
+    locate_term qid @
+    locate_modtype qid @
+    locate_module qid @
+    String.Map.fold (fun s _ accu -> locate_other s qid @ accu) !locatable_map []
+  in
+  match located with
+    | [] ->
+        let (dir,id) = repr_qualid qid in
+        if DirPath.is_empty dir then
+          str "No " ++ str name ++ str " of basename" ++ spc () ++ Id.print id
+        else
+          str "No " ++ str name ++ str " of suffix" ++ spc () ++ pr_qualid qid
+    | l ->
+        prlist_with_sep fnl
+        (fun (o,oqid) ->
+          hov 2 (pr_located_qualid o ++
+          (if not (qualid_eq oqid qid) then
+            spc() ++ str "(shorter name to refer to it in current context is "
+            ++ pr_qualid oqid ++ str")"
+           else mt ()) ++
+          display_alias o)) l
+
+let print_located_term ref = print_located_qualid "term" LocTerm ref
+let print_located_other s ref = print_located_qualid s (LocOther s) ref
+let print_located_module ref = print_located_qualid "module" LocModule ref
+let print_located_qualid ref = print_located_qualid "object" LocAny ref
+
+(******************************************)
+(**** Printing declarations and judgments *)
+(****  Gallina layer                  *****)
+
+let gallina_print_typed_value_in_env env sigma (trm,typ) =
+  (pr_leconstr_env env sigma trm ++ fnl () ++
+     str "     : " ++ pr_letype_env env sigma typ)
+
+(* To be improved; the type should be used to provide the types in the
+   abstractions. This should be done recursively inside pr_lconstr, so that
+   the pretty-print of a proposition (P:(nat->nat)->Prop)(P [u]u)
+   synthesizes the type nat of the abstraction on u *)
+
+let print_named_def env sigma name body typ =
+  let pbody = pr_lconstr_env env sigma body in
+  let ptyp = pr_ltype_env env sigma typ in
+  let pbody = if Constr.isCast body then surround pbody else pbody in
+  (str "*** [" ++ str name ++ str " " ++
+     hov 0 (str ":=" ++ brk (1,2) ++ pbody ++ spc () ++
+              str ":" ++ brk (1,2) ++ ptyp) ++
+           str "]")
+
+let print_named_assum env sigma name typ =
+  str "*** [" ++ str name ++ str " : " ++ pr_ltype_env env sigma typ ++ str "]"
+
+let gallina_print_named_decl env sigma =
+  let open Context.Named.Declaration in
+  function
+  | LocalAssum (id, typ) ->
+     print_named_assum env sigma (Id.to_string id.Context.binder_name) typ
+  | LocalDef (id, body, typ) ->
+     print_named_def env sigma (Id.to_string id.Context.binder_name) body typ
+
+let assumptions_for_print lna =
+  List.fold_right (fun na env -> add_name na env) lna empty_names_context
+
+(*********************)
+(* *)
+
+let gallina_print_inductive sp udecl =
+  let env = Global.env() in
+  let mib = Environ.lookup_mind sp env in
+  let mipv = mib.mind_packets in
+  pr_mutual_inductive_body env sp mib udecl ++
+  with_line_skip
+    (print_primitive_record mib.mind_finite mipv mib.mind_record @
+     print_inductive_renames sp mipv @
+     print_inductive_implicit_args sp mipv @
+     print_inductive_argument_scopes sp mipv)
+
+let print_named_decl env sigma id =
+  gallina_print_named_decl env sigma (Global.lookup_named id) ++ fnl ()
+
+let gallina_print_section_variable env sigma id =
+  print_named_decl env sigma id ++
+  with_line_skip (print_name_infos (GlobRef.VarRef id))
+
+let print_body env evd = function
+  | Some c  -> pr_lconstr_env env evd c
+  | None -> (str"<no body>")
+
+let print_typed_body env evd (val_0,typ) =
+  (print_body env evd val_0 ++ fnl () ++ str "     : " ++ pr_ltype_env env evd typ)
+
+let print_instance sigma cb =
+  if Declareops.constant_is_polymorphic cb then
+    let univs = Declareops.constant_polymorphic_context cb in
+    let inst = Univ.make_abstract_instance univs in
+    pr_universe_instance sigma inst
+  else mt()
+
+let print_constant indirect_accessor with_values sep sp udecl =
+  let cb = Global.lookup_constant sp in
+  let val_0 = Global.body_of_constant_body indirect_accessor cb in
+  let typ = cb.const_type in
+  let univs =
+    let open Univ in
+    let otab = Global.opaque_tables () in
+    match cb.const_body with
+    | Undef _ | Def _ | Primitive _ -> cb.const_universes
+    | OpaqueDef o ->
+      let body_uctxs = Opaqueproof.force_constraints indirect_accessor otab o in
+      match cb.const_universes with
+      | Monomorphic ctx ->
+        Monomorphic (ContextSet.union body_uctxs ctx)
+      | Polymorphic ctx ->
+        assert(ContextSet.is_empty body_uctxs);
+        Polymorphic ctx
+  in
+  let ctx =
+    UState.of_binders
+      (UnivNames.universe_binders_with_opt_names (Declareops.constant_polymorphic_context cb) udecl)
+  in
+  let env = Global.env () and sigma = Evd.from_ctx ctx in
+  let pr_ltype = pr_ltype_env env sigma in
+  hov 0 (
+    match val_0 with
+    | None ->
+        str"*** [ " ++
+        print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++
+        str" ]" ++
+        Printer.pr_universes sigma univs
+    | Some (c, priv, ctx) ->
+      let priv = match priv with
+      | Opaqueproof.PrivateMonomorphic () -> None
+      | Opaqueproof.PrivatePolymorphic (_, ctx) -> Some ctx
+      in
+        print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++
+        (if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++
+        Printer.pr_universes sigma univs ?priv)
+
+let gallina_print_constant_with_infos indirect_accessor sp udecl =
+  print_constant indirect_accessor true " = " sp udecl ++
+  with_line_skip (print_name_infos (GlobRef.ConstRef sp))
+
+let gallina_print_syntactic_def env kn =
+  let qid = Nametab.shortest_qualid_of_syndef Id.Set.empty kn
+  and (vars,a) = Syntax_def.search_syntactic_definition kn in
+  let c = Notation_ops.glob_constr_of_notation_constr a in
+  hov 2
+    (hov 4
+       (str "Notation " ++ pr_qualid qid ++
+        prlist (fun id -> spc () ++ Id.print id) (List.map fst vars) ++
+        spc () ++ str ":=") ++
+     spc () ++
+     Constrextern.without_specific_symbols
+       [Notation.SynDefRule kn] (pr_glob_constr_env env) c)
+
+let gallina_print_leaf_entry ~mod_ops indirect_accessor env sigma with_values ((sp,kn as oname),lobj) =
+  let sep = if with_values then " = " else " : " in
+  match lobj with
+  | AtomicObject o ->
+    let tag = object_tag o in
+    begin match (oname,tag) with
+      | (_,"VARIABLE") ->
+          (* Outside sections, VARIABLES still exist but only with universes
+             constraints *)
+          (try Some(print_named_decl env sigma (basename sp)) with Not_found -> None)
+      | (_,"CONSTANT") ->
+          Some (print_constant indirect_accessor with_values sep (Constant.make1 kn) None)
+      | (_,"INDUCTIVE") ->
+          Some (gallina_print_inductive (MutInd.make1 kn) None)
+      | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"|
+            "COERCION"|"REQUIRE"|"END-SECTION"|"STRUCTURE")) -> None
+      (* To deal with forgotten cases... *)
+      | (_,s) -> None
+    end
+  | ModuleObject _ ->
+    let (mp,l) = KerName.repr kn in
+    Some (print_module ~mod_ops with_values (MPdot (mp,l)))
+  | ModuleTypeObject _ ->
+    let (mp,l) = KerName.repr kn in
+          Some (print_modtype ~mod_ops (MPdot (mp,l)))
+  | _ -> None
+
+let gallina_print_library_entry ~mod_ops indirect_accessor env sigma with_values ent =
+  let pr_name (sp,_) = Id.print (basename sp) in
+  match ent with
+    | (oname,Lib.Leaf lobj) ->
+      gallina_print_leaf_entry ~mod_ops indirect_accessor env sigma with_values (oname,lobj)
+    | (oname,Lib.OpenedSection (dir,_)) ->
+      Some (str " >>>>>>> Section " ++ pr_name oname)
+    | (_,Lib.CompilingLibrary { Nametab.obj_dir; _ }) ->
+      Some (str " >>>>>>> Library " ++ DirPath.print obj_dir)
+    | (oname,Lib.OpenedModule _) ->
+      Some (str " >>>>>>> Module " ++ pr_name oname)
+
+let gallina_print_context ~mod_ops indirect_accessor env sigma with_values =
+  let rec prec n = function
+    | h::rest when Option.is_empty n || Option.get n > 0 ->
+      (match gallina_print_library_entry ~mod_ops indirect_accessor env sigma with_values h with
+       | None -> prec n rest
+       | Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ())
+    | _ -> mt ()
+  in
+  prec
+
+let gallina_print_eval red_fun env sigma _ {uj_val=trm;uj_type=typ} =
+  let ntrm = red_fun env sigma trm in
+  (str "     = " ++ gallina_print_typed_value_in_env env sigma (ntrm,typ))
+
+(******************************************)
+(**** Printing abstraction layer          *)
+
+let default_object_pr = {
+  print_inductive           = gallina_print_inductive;
+  print_constant_with_infos = gallina_print_constant_with_infos;
+  print_section_variable    = gallina_print_section_variable;
+  print_syntactic_def       = gallina_print_syntactic_def;
+  print_module              = gallina_print_module;
+  print_modtype             = gallina_print_modtype;
+  print_named_decl          = gallina_print_named_decl;
+  print_library_entry       = gallina_print_library_entry;
+  print_context             = gallina_print_context;
+  print_typed_value_in_env  = gallina_print_typed_value_in_env;
+  print_eval                = gallina_print_eval;
+}
+
+let object_pr = ref default_object_pr
+let set_object_pr = (:=) object_pr
+
+let print_inductive x = !object_pr.print_inductive x
+let print_constant_with_infos c = !object_pr.print_constant_with_infos c
+let print_section_variable c = !object_pr.print_section_variable c
+let print_syntactic_def x = !object_pr.print_syntactic_def x
+let print_module x  = !object_pr.print_module  x
+let print_modtype x = !object_pr.print_modtype x
+let print_named_decl x = !object_pr.print_named_decl x
+let print_library_entry ~mod_ops x = !object_pr.print_library_entry ~mod_ops x
+let print_context ~mod_ops x = !object_pr.print_context ~mod_ops x
+let print_typed_value_in_env x = !object_pr.print_typed_value_in_env x
+let print_eval x = !object_pr.print_eval x
+
+(******************************************)
+(**** Printing declarations and judgments *)
+(****  Abstract layer                 *****)
+
+let print_judgment env sigma {uj_val=trm;uj_type=typ} =
+  print_typed_value_in_env env sigma (trm, typ)
+
+let print_safe_judgment env sigma j =
+  let trm = Safe_typing.j_val j in
+  let typ = Safe_typing.j_type j in
+  let trm = EConstr.of_constr trm in
+  let typ = EConstr.of_constr typ in
+  print_typed_value_in_env env sigma (trm, typ)
+
+(*********************)
+(* *)
+
+let print_full_context ~mod_ops indirect_accessor env sigma =
+  print_context ~mod_ops indirect_accessor env sigma true None (Lib.contents ())
+let print_full_context_typ ~mod_ops indirect_accessor env sigma =
+  print_context ~mod_ops indirect_accessor env sigma false None (Lib.contents ())
+
+let print_full_pure_context ~mod_ops ~library_accessor env sigma =
+  let rec prec = function
+  | ((_,kn),Lib.Leaf AtomicObject lobj)::rest ->
+      let pp = match object_tag lobj with
+      | "CONSTANT" ->
+          let con = Global.constant_of_delta_kn kn in
+          let cb = Global.lookup_constant con in
+          let typ = cb.const_type in
+          hov 0 (
+            match cb.const_body with
+              | Undef _ ->
+                str "Parameter " ++
+                print_basename con ++ str " : " ++ cut () ++ pr_ltype_env env sigma typ
+              | OpaqueDef lc ->
+                str "Theorem " ++ print_basename con ++ cut () ++
+                str " : " ++ pr_ltype_env env sigma typ ++ str "." ++ fnl () ++
+                str "Proof " ++ pr_lconstr_env env sigma (fst (Opaqueproof.force_proof library_accessor (Global.opaque_tables ()) lc))
+              | Def c ->
+                str "Definition " ++ print_basename con ++ cut () ++
+                str "  : " ++ pr_ltype_env env sigma typ ++ cut () ++ str " := " ++
+                pr_lconstr_env env sigma (Mod_subst.force_constr c)
+              | Primitive _ ->
+                 str "Primitive " ++
+                   print_basename con ++ str " : " ++ cut () ++ pr_ltype_env env sigma typ)
+          ++ str "." ++ fnl () ++ fnl ()
+      | "INDUCTIVE" ->
+          let mind = Global.mind_of_delta_kn kn in
+          let mib = Global.lookup_mind mind in
+          pr_mutual_inductive_body (Global.env()) mind mib None ++
+            str "." ++ fnl () ++ fnl ()
+      | _ -> mt () in
+      prec rest ++ pp
+  | ((_,kn),Lib.Leaf ModuleObject _)::rest ->
+          (* TODO: make it reparsable *)
+    let (mp,l) = KerName.repr kn in
+          prec rest ++ print_module ~mod_ops true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl ()
+  | ((_,kn),Lib.Leaf ModuleTypeObject _)::rest ->
+          (* TODO: make it reparsable *)
+    let (mp,l) = KerName.repr kn in
+          prec rest ++ print_modtype ~mod_ops (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl ()
+  | _::rest -> prec rest
+  | _ -> mt () in
+  prec (Lib.contents ())
+
+(* For printing an inductive definition with
+   its constructors and elimination,
+   assume that the declaration of constructors and eliminations
+   follows the definition of the inductive type *)
+
+(* This is designed to print the contents of an opened section *)
+let read_sec_context qid =
+  let dir =
+    try Nametab.locate_section qid
+    with Not_found ->
+      user_err ?loc:qid.loc ~hdr:"read_sec_context" (str "Unknown section.") in
+  let rec get_cxt in_cxt = function
+    | (_,Lib.OpenedSection ({Nametab.obj_dir;_},_) as hd)::rest ->
+        if DirPath.equal dir obj_dir then (hd::in_cxt) else get_cxt (hd::in_cxt) rest
+    | [] -> []
+    | hd::rest -> get_cxt (hd::in_cxt) rest
+  in
+  let cxt = Lib.contents () in
+  List.rev (get_cxt [] cxt)
+
+let print_sec_context ~mod_ops indirect_accessor env sigma sec =
+  print_context ~mod_ops indirect_accessor env sigma true None (read_sec_context sec)
+
+let print_sec_context_typ ~mod_ops indirect_accessor env sigma sec =
+  print_context ~mod_ops indirect_accessor env sigma false None (read_sec_context sec)
+
+let maybe_error_reject_univ_decl na udecl =
+  let open GlobRef in
+  match na, udecl with
+  | _, None | Term (ConstRef _ | IndRef _ | ConstructRef _), Some _ -> ()
+  | (Term (VarRef _) | Syntactic _ | Dir _ | ModuleType _ | Other _ | Undefined _), Some udecl ->
+    (* TODO Print na somehow *)
+    user_err ~hdr:"reject_univ_decl" (str "This object does not support universe names.")
+
+let print_any_name ~mod_ops indirect_accessor env sigma na udecl =
+  maybe_error_reject_univ_decl na udecl;
+  let open GlobRef in
+  match na with
+  | Term (ConstRef sp) -> print_constant_with_infos indirect_accessor sp udecl
+  | Term (IndRef (sp,_)) -> print_inductive sp udecl
+  | Term (ConstructRef ((sp,_),_)) -> print_inductive sp udecl
+  | Term (VarRef sp) -> print_section_variable env sigma sp
+  | Syntactic kn -> print_syntactic_def env kn
+  | Dir (Nametab.GlobDirRef.DirModule Nametab.{ obj_dir; obj_mp; _ } ) ->
+    print_module ~mod_ops (printable_body obj_dir) obj_mp
+  | Dir _ -> mt ()
+  | ModuleType mp -> print_modtype ~mod_ops mp
+  | Other (obj, info) -> info.print obj
+  | Undefined qid ->
+  try  (* Var locale de but, pas var de section... donc pas d'implicits *)
+    let dir,str = repr_qualid qid in
+    if not (DirPath.is_empty dir) then raise Not_found;
+    str |> Global.lookup_named |> print_named_decl env sigma
+
+  with Not_found ->
+    user_err
+      ~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.")
+
+let print_name ~mod_ops indirect_accessor env sigma na udecl =
+  match na with
+  | {loc; v=Constrexpr.ByNotation (ntn,sc)} ->
+    print_any_name ~mod_ops indirect_accessor env sigma
+      (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
+               ntn sc))
+      udecl
+  | {loc; v=Constrexpr.AN ref} ->
+    print_any_name ~mod_ops indirect_accessor env sigma (locate_any_name ref) udecl
+
+let print_opaque_name indirect_accessor env sigma qid =
+  let open GlobRef in
+  match Nametab.global qid with
+    | ConstRef cst ->
+      let cb = Global.lookup_constant cst in
+      if Declareops.constant_has_body cb then
+        print_constant_with_infos indirect_accessor cst None
+      else
+        user_err Pp.(str "Not a defined constant.")
+    | IndRef (sp,_) ->
+      print_inductive sp None
+    | ConstructRef cstr as gr ->
+      let ty, ctx = Typeops.type_of_global_in_context env gr in
+      let ty = EConstr.of_constr ty in
+      let open EConstr in
+      print_typed_value_in_env env sigma (mkConstruct cstr, ty)
+    | VarRef id ->
+      env |> lookup_named id |> print_named_decl env sigma
+
+let print_about_any ?loc env sigma k udecl =
+  maybe_error_reject_univ_decl k udecl;
+  match k with
+  | Term ref ->
+    let rb = Reductionops.ReductionBehaviour.print ref in
+    Dumpglob.add_glob ?loc ref;
+      pr_infos_list
+       (print_ref false ref udecl :: blankline ::
+        print_polymorphism ref @
+        print_name_infos ref @
+        (if Pp.ismt rb then [] else [rb]) @
+        print_opacity ref @
+  print_bidi_hints ref @
+  [hov 0 (str "Expands to: " ++ pr_located_qualid k)])
+  | Syntactic kn ->
+    let () = match Syntax_def.search_syntactic_definition kn with
+    | [],Notation_term.NRef ref -> Dumpglob.add_glob ?loc ref
+    | _ -> () in
+      v 0 (
+      print_syntactic_def env kn ++ fnl () ++
+      hov 0 (str "Expands to: " ++ pr_located_qualid k))
+  | Dir _ | ModuleType _ | Undefined _ ->
+      hov 0 (pr_located_qualid k)
+  | Other (obj, info) -> hov 0 (info.about obj)
+
+let print_about env sigma na udecl =
+  match na with
+  | {loc;v=Constrexpr.ByNotation (ntn,sc)} ->
+      print_about_any ?loc env sigma
+        (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
+               ntn sc)) udecl
+  | {loc;v=Constrexpr.AN ref} ->
+      print_about_any ?loc env sigma (locate_any_name ref) udecl
+
+(* for debug *)
+let inspect ~mod_ops indirect_accessor env sigma depth =
+  print_context ~mod_ops indirect_accessor env sigma false (Some depth) (Lib.contents ())
+
+(*************************************************************************)
+(* Pretty-printing functions coming from classops.ml                     *)
+
+open Classops
+
+let print_coercion_value v = Printer.pr_global v.coe_value
+
+let print_class i =
+  let cl,_ = class_info_from_index i in
+  pr_class cl
+
+let print_path ((i,j),p) =
+  hov 2 (
+    str"[" ++ hov 0 (prlist_with_sep pr_semicolon print_coercion_value p) ++
+    str"] : ") ++
+  print_class i ++ str" >-> " ++ print_class j
+
+let _ = Classops.install_path_printer print_path
+
+let print_graph () =
+  prlist_with_sep fnl print_path (inheritance_graph())
+
+let print_classes () =
+  pr_sequence pr_class (classes())
+
+let print_coercions () =
+  pr_sequence print_coercion_value (coercions())
+
+let index_of_class cl =
+  try
+    fst (class_info cl)
+  with Not_found ->
+    user_err ~hdr:"index_of_class"
+      (pr_class cl ++ spc() ++ str "not a defined class.")
+
+let print_path_between cls clt =
+  let i = index_of_class cls in
+  let j = index_of_class clt in
+  let p =
+    try
+      lookup_path_between_class (i,j)
+    with Not_found ->
+      user_err ~hdr:"index_cl_of_id"
+        (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt
+         ++ str ".")
+  in
+  print_path ((i,j),p)
+
+let print_canonical_projections env sigma =
+  prlist_with_sep fnl
+    (fun ((r1,r2),o) -> pr_cs_pattern r2 ++
+    str " <- " ++
+    pr_global r1 ++ str " ( " ++ pr_lconstr_env env sigma o.o_DEF ++ str " )")
+    (canonical_projections ())
+
+(*************************************************************************)
+
+(*************************************************************************)
+(* Pretty-printing functions for type classes                     *)
+
+open Typeclasses
+
+let pr_typeclass env t =
+  print_ref false t.cl_impl None
+
+let print_typeclasses () =
+  let env = Global.env () in
+    prlist_with_sep fnl (pr_typeclass env) (typeclasses ())
+
+let pr_instance env i =
+  (*   gallina_print_constant_with_infos i.is_impl *)
+  (* lighter *)
+  print_ref false (instance_impl i) None ++
+  begin match hint_priority i with
+  | None -> mt ()
+  | Some i -> spc () ++ str "|" ++ spc () ++ int i
+  end
+
+let print_all_instances () =
+  let env = Global.env () in
+  let inst = all_instances () in
+    prlist_with_sep fnl (pr_instance env) inst
+
+let print_instances r =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  let inst = instances env sigma r in
+    prlist_with_sep fnl (pr_instance env) inst
diff --git a/vernac/prettyp.mli b/vernac/prettyp.mli
new file mode 100644
index 0000000000..c8b361d95b
--- /dev/null
+++ b/vernac/prettyp.mli
@@ -0,0 +1,129 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Names
+open Environ
+open Reductionops
+open Libnames
+
+(** A Pretty-Printer for the Calculus of Inductive Constructions. *)
+
+val assumptions_for_print : Name.t list -> Termops.names_context
+
+val print_closed_sections : bool ref
+val print_context
+  : mod_ops:Printmod.mod_ops
+  -> Opaqueproof.indirect_accessor
+  -> env -> Evd.evar_map
+  -> bool -> int option -> Lib.library_segment -> Pp.t
+val print_library_entry
+  : mod_ops:Printmod.mod_ops
+  -> Opaqueproof.indirect_accessor
+  -> env -> Evd.evar_map
+  -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option
+val print_full_context
+  : mod_ops:Printmod.mod_ops
+  -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t
+val print_full_context_typ
+  : mod_ops:Printmod.mod_ops
+  -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t
+
+val print_full_pure_context
+  : mod_ops:Printmod.mod_ops
+  -> library_accessor:Opaqueproof.indirect_accessor
+  -> env
+  -> Evd.evar_map
+  -> Pp.t
+
+val print_sec_context
+  : mod_ops:Printmod.mod_ops
+  -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t
+val print_sec_context_typ
+  : mod_ops:Printmod.mod_ops
+  -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t
+val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> Pp.t
+val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> Pp.t
+val print_eval :
+  reduction_function -> env -> Evd.evar_map ->
+    Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t
+
+val print_name
+  : mod_ops:Printmod.mod_ops
+  -> Opaqueproof.indirect_accessor
+  -> env -> Evd.evar_map -> qualid Constrexpr.or_by_notation
+  -> UnivNames.univ_name_list option -> Pp.t
+val print_opaque_name
+  : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t
+val print_about : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation ->
+  UnivNames.univ_name_list option -> Pp.t
+val print_impargs : qualid Constrexpr.or_by_notation -> Pp.t
+
+(** Pretty-printing functions for classes and coercions *)
+val print_graph : unit -> Pp.t
+val print_classes : unit -> Pp.t
+val print_coercions : unit -> Pp.t
+val print_path_between : Classops.cl_typ -> Classops.cl_typ -> Pp.t
+val print_canonical_projections : env -> Evd.evar_map -> Pp.t
+
+(** Pretty-printing functions for type classes and instances *)
+val print_typeclasses : unit -> Pp.t
+val print_instances : GlobRef.t -> Pp.t
+val print_all_instances : unit -> Pp.t
+
+val inspect
+  : mod_ops:Printmod.mod_ops
+  -> Opaqueproof.indirect_accessor
+  -> env -> Evd.evar_map -> int -> Pp.t
+
+(** {5 Locate} *)
+
+type 'a locatable_info = {
+  locate : qualid -> 'a option;
+  (** Locate the most precise object with the provided name if any. *)
+  locate_all : qualid -> 'a list;
+  (** Locate all objects whose name is a suffix of the provided name *)
+  shortest_qualid : 'a -> qualid;
+  (** Return the shortest name in the current context *)
+  name : 'a -> Pp.t;
+  (** Data as printed by the Locate command *)
+  print : 'a -> Pp.t;
+  (** Data as printed by the Print command *)
+  about : 'a -> Pp.t;
+  (** Data as printed by the About command *)
+}
+(** Generic data structure representing locatable objects. *)
+
+val register_locatable : string -> 'a locatable_info -> unit
+(** Define a new type of locatable objects that can be reached via the
+    corresponding generic vernacular commands. The string should be a unique
+    name describing the kind of objects considered and that is added as a
+    grammar command prefix for vernacular commands Locate. *)
+
+val print_located_qualid : qualid -> Pp.t
+val print_located_term : qualid -> Pp.t
+val print_located_module : qualid -> Pp.t
+val print_located_other : string -> qualid -> Pp.t
+
+type object_pr = {
+  print_inductive           : MutInd.t -> UnivNames.univ_name_list option -> Pp.t;
+  print_constant_with_infos : Opaqueproof.indirect_accessor -> Constant.t -> UnivNames.univ_name_list option -> Pp.t;
+  print_section_variable    : env -> Evd.evar_map -> variable -> Pp.t;
+  print_syntactic_def       : env -> KerName.t -> Pp.t;
+  print_module              : mod_ops:Printmod.mod_ops -> bool -> ModPath.t -> Pp.t;
+  print_modtype             : mod_ops:Printmod.mod_ops -> ModPath.t -> Pp.t;
+  print_named_decl          : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t;
+  print_library_entry       : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option;
+  print_context             : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t;
+  print_typed_value_in_env  : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t;
+  print_eval                : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t;
+}
+
+val set_object_pr : object_pr -> unit
+val default_object_pr : object_pr
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 102da20257..7563b4a5d5 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -10,6 +10,7 @@ Locality
 Egramml
 Vernacextend
 Ppvernac
+Prettyp
 Proof_using
 Egramcoq
 Metasyntax