diff options
| -rw-r--r-- | dev/ci/user-overlays/10727-ejgallego-library+to_vernac_step2.sh | 6 | ||||
| -rw-r--r-- | interp/modintern.ml | 6 | ||||
| -rw-r--r-- | interp/modintern.mli | 4 | ||||
| -rw-r--r-- | library/library.mllib | 1 | ||||
| -rw-r--r-- | printing/prettyp.ml | 63 | ||||
| -rw-r--r-- | printing/prettyp.mli | 37 | ||||
| -rw-r--r-- | printing/printmod.ml | 75 | ||||
| -rw-r--r-- | printing/printmod.mli | 10 | ||||
| -rw-r--r-- | toplevel/coqc.ml | 5 | ||||
| -rw-r--r-- | vernac/declaremods.ml (renamed from library/declaremods.ml) | 116 | ||||
| -rw-r--r-- | vernac/declaremods.mli (renamed from library/declaremods.mli) | 47 | ||||
| -rw-r--r-- | vernac/himsg.ml | 4 | ||||
| -rw-r--r-- | vernac/vernac.mllib | 1 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 40 |
14 files changed, 209 insertions, 206 deletions
diff --git a/dev/ci/user-overlays/10727-ejgallego-library+to_vernac_step2.sh b/dev/ci/user-overlays/10727-ejgallego-library+to_vernac_step2.sh new file mode 100644 index 0000000000..a5f6551474 --- /dev/null +++ b/dev/ci/user-overlays/10727-ejgallego-library+to_vernac_step2.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10727" ] || [ "$CI_BRANCH" = "library+to_vernac_step2" ]; then + + elpi_CI_REF=library+to_vernac_step2 + elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi + +fi diff --git a/interp/modintern.ml b/interp/modintern.ml index 955288244e..ddf5b2d7b1 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -12,7 +12,6 @@ open Declarations open Libnames open Constrexpr open Constrintern -open Declaremods type module_internalization_error = | NotAModuleNorModtype of string @@ -21,9 +20,11 @@ type module_internalization_error = exception ModuleInternalizationError of module_internalization_error +type module_kind = Module | ModType | ModAny + let error_not_a_module_loc kind loc qid = let s = string_of_qualid qid in - let e = let open Declaremods in match kind with + let e = match kind with | Module -> Modops.ModuleTypingError (Modops.NotAModule s) | ModType -> Modops.ModuleTypingError (Modops.NotAModuleType s) | ModAny -> ModuleInternalizationError (NotAModuleNorModtype s) @@ -46,7 +47,6 @@ let error_application_to_module_type loc = it is equal to the input kind when this one isn't ModAny. *) let lookup_module_or_modtype kind qid = - let open Declaremods in let loc = qid.CAst.loc in try if kind == ModType then raise Not_found; diff --git a/interp/modintern.mli b/interp/modintern.mli index 75ab38c64a..72695a680e 100644 --- a/interp/modintern.mli +++ b/interp/modintern.mli @@ -28,5 +28,7 @@ exception ModuleInternalizationError of module_internalization_error kind is never ModAny, and it is equal to the input kind when this one isn't ModAny. *) +type module_kind = Module | ModType | ModAny + val interp_module_ast : - env -> Declaremods.module_kind -> module_ast -> module_struct_entry * Declaremods.module_kind * Univ.ContextSet.t + env -> module_kind -> module_ast -> module_struct_entry * module_kind * Univ.ContextSet.t diff --git a/library/library.mllib b/library/library.mllib index c34d8911e8..a6188f7661 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -5,7 +5,6 @@ Summary Nametab Global Lib -Declaremods States Kindops Goptions diff --git a/printing/prettyp.ml b/printing/prettyp.ml index fb0b1eca8d..c995887f31 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -38,11 +38,11 @@ type object_pr = { 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 : bool -> ModPath.t -> Pp.t; - print_modtype : ModPath.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 : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; - print_context : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> 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; } @@ -618,7 +618,7 @@ let gallina_print_syntactic_def env kn = Constrextern.without_specific_symbols [Notation.SynDefRule kn] (pr_glob_constr_env env) c) -let gallina_print_leaf_entry indirect_accessor env sigma with_values ((sp,kn as oname),lobj) = +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 -> @@ -639,17 +639,17 @@ let gallina_print_leaf_entry indirect_accessor env sigma with_values ((sp,kn as end | ModuleObject _ -> let (mp,l) = KerName.repr kn in - Some (print_module with_values (MPdot (mp,l))) + Some (print_module ~mod_ops with_values (MPdot (mp,l))) | ModuleTypeObject _ -> let (mp,l) = KerName.repr kn in - Some (print_modtype (MPdot (mp,l))) + Some (print_modtype ~mod_ops (MPdot (mp,l))) | _ -> None -let gallina_print_library_entry indirect_accessor env sigma with_values ent = +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 indirect_accessor env sigma with_values (oname,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; _ }) -> @@ -657,10 +657,10 @@ let gallina_print_library_entry indirect_accessor env sigma with_values ent = | (oname,Lib.OpenedModule _) -> Some (str " >>>>>>> Module " ++ pr_name oname) -let gallina_print_context indirect_accessor env sigma with_values = +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 indirect_accessor env sigma with_values h with + (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 () @@ -698,8 +698,8 @@ 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 x = !object_pr.print_library_entry x -let print_context x = !object_pr.print_context 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 @@ -720,10 +720,12 @@ let print_safe_judgment env sigma j = (*********************) (* *) -let print_full_context indirect_accessor env sigma = print_context indirect_accessor env sigma true None (Lib.contents ()) -let print_full_context_typ indirect_accessor env sigma = print_context indirect_accessor env sigma false None (Lib.contents ()) +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 ~library_accessor env sigma = +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 @@ -758,11 +760,11 @@ let print_full_pure_context ~library_accessor env sigma = | ((_,kn),Lib.Leaf ModuleObject _)::rest -> (* TODO: make it reparsable *) let (mp,l) = KerName.repr kn in - prec rest ++ print_module true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () + 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 (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () + prec rest ++ print_modtype ~mod_ops (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () | _::rest -> prec rest | _ -> mt () in prec (Lib.contents ()) @@ -787,11 +789,11 @@ let read_sec_context qid = let cxt = Lib.contents () in List.rev (get_cxt [] cxt) -let print_sec_context indirect_accessor env sigma sec = - print_context indirect_accessor env sigma true None (read_sec_context sec) +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 indirect_accessor env sigma sec = - print_context indirect_accessor env sigma false 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 @@ -801,7 +803,7 @@ let maybe_error_reject_univ_decl na udecl = (* TODO Print na somehow *) user_err ~hdr:"reject_univ_decl" (str "This object does not support universe names.") -let print_any_name indirect_accessor env sigma na udecl = +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 @@ -810,9 +812,10 @@ let print_any_name indirect_accessor env sigma na 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 (printable_body obj_dir) obj_mp + | 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 mp + | 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 *) @@ -824,15 +827,15 @@ let print_any_name indirect_accessor env sigma na udecl = user_err ~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") -let print_name indirect_accessor env sigma na udecl = +let print_name ~mod_ops indirect_accessor env sigma na udecl = match na with | {loc; v=Constrexpr.ByNotation (ntn,sc)} -> - print_any_name indirect_accessor env sigma + 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 indirect_accessor env sigma (locate_any_name ref) udecl + 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 @@ -888,8 +891,8 @@ let print_about env sigma na udecl = print_about_any ?loc env sigma (locate_any_name ref) udecl (* for debug *) -let inspect indirect_accessor env sigma depth = - print_context indirect_accessor env sigma false (Some depth) (Lib.contents ()) +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 *) diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 4299bcc880..c8b361d95b 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -19,28 +19,35 @@ val assumptions_for_print : Name.t list -> Termops.names_context val print_closed_sections : bool ref val print_context - : Opaqueproof.indirect_accessor + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t val print_library_entry - : Opaqueproof.indirect_accessor + : 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 - : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t val print_full_context_typ - : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t val print_full_pure_context - : library_accessor:Opaqueproof.indirect_accessor + : mod_ops:Printmod.mod_ops + -> library_accessor:Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t val print_sec_context - : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t val print_sec_context_typ - : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t + : 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 : @@ -48,7 +55,8 @@ val print_eval : Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t val print_name - : Opaqueproof.indirect_accessor + : 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 @@ -69,7 +77,10 @@ val print_typeclasses : unit -> Pp.t val print_instances : GlobRef.t -> Pp.t val print_all_instances : unit -> Pp.t -val inspect : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> int -> Pp.t +val inspect + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor + -> env -> Evd.evar_map -> int -> Pp.t (** {5 Locate} *) @@ -105,11 +116,11 @@ type object_pr = { 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 : bool -> ModPath.t -> Pp.t; - print_modtype : ModPath.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 : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option; - print_context : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> 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; } diff --git a/printing/printmod.ml b/printing/printmod.ml index 141469ff9c..03921bca30 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -240,9 +240,14 @@ let nametab_register_body mp dir (l,body) = mip.mind_consnames) mib.mind_packets -let nametab_register_module_body mp struc = +type mod_ops = + { import_module : export:bool -> ModPath.t -> unit + ; process_module_binding : MBId.t -> Declarations.module_alg_expr -> unit + } + +let nametab_register_module_body ~mod_ops mp struc = (* If [mp] is a globally visible module, we simply import it *) - try Declaremods.import_module ~export:false mp + try mod_ops.import_module ~export:false mp with Not_found -> (* Otherwise we try to emulate an import by playing with nametab *) nametab_register_dir mp; @@ -252,7 +257,7 @@ let get_typ_expr_alg mtb = match mtb.mod_type_alg with | Some (NoFunctor me) -> me | _ -> raise Not_found -let nametab_register_modparam mbid mtb = +let nametab_register_modparam ~mod_ops mbid mtb = let id = MBId.to_id mbid in match mtb.mod_type with | MoreFunctor _ -> id (* functorial param : nothing to register *) @@ -260,7 +265,7 @@ let nametab_register_modparam mbid mtb = (* We first try to use the algebraic type expression if any, via a Declaremods function that converts back to module entries *) try - let () = Declaremods.process_module_binding mbid (get_typ_expr_alg mtb) in + let () = mod_ops.process_module_binding mbid (get_typ_expr_alg mtb) in id with e when CErrors.noncritical e -> (* Otherwise, we try to play with the nametab ourselves *) @@ -314,9 +319,9 @@ let print_body is_impl extent env mp (l,body) = let print_struct is_impl extent env mp struc = prlist_with_sep spc (print_body is_impl extent env mp) struc -let print_structure is_type extent env mp locals struc = +let print_structure ~mod_ops is_type extent env mp locals struc = let env' = Modops.add_structure mp struc Mod_subst.empty_delta_resolver env in - nametab_register_module_body mp struc; + nametab_register_module_body ~mod_ops mp struc; let kwd = if is_type then "Sig" else "Struct" in hv 2 (keyword kwd ++ spc () ++ print_struct false extent env' mp struc ++ brk (1,-2) ++ keyword "End") @@ -362,31 +367,31 @@ let print_mod_expr env mp locals = function (str"(" ++ prlist_with_sep spc (print_modpath locals) lapp ++ str")") | MEwith _ -> assert false (* No 'with' syntax for modules *) -let rec print_functor fty fatom is_type extent env mp locals = function - | NoFunctor me -> fatom is_type extent env mp locals me +let rec print_functor ~mod_ops fty fatom is_type extent env mp locals = function + | NoFunctor me -> fatom ~mod_ops is_type extent env mp locals me | MoreFunctor (mbid,mtb1,me2) -> - let id = nametab_register_modparam mbid mtb1 in + let id = nametab_register_modparam ~mod_ops mbid mtb1 in let mp1 = MPbound mbid in - let pr_mtb1 = fty extent env mp1 locals mtb1 in + let pr_mtb1 = fty ~mod_ops extent env mp1 locals mtb1 in let env' = Modops.add_module_type mp1 mtb1 env in let locals' = (mbid, get_new_id locals (MBId.to_id mbid))::locals in let kwd = if is_type then "Funsig" else "Functor" in hov 2 (keyword kwd ++ spc () ++ str "(" ++ Id.print id ++ str ":" ++ pr_mtb1 ++ str ")" ++ - spc() ++ print_functor fty fatom is_type extent env' mp locals' me2) + spc() ++ print_functor ~mod_ops fty fatom is_type extent env' mp locals' me2) -let rec print_expression x = - print_functor +let rec print_expression ~mod_ops x = + print_functor ~mod_ops print_modtype - (function true -> print_typ_expr | false -> fun _ -> print_mod_expr) x + (fun ~mod_ops -> function true -> print_typ_expr | false -> fun _ -> print_mod_expr) x -and print_signature x = - print_functor print_modtype print_structure x +and print_signature ~mod_ops x = + print_functor ~mod_ops print_modtype print_structure x -and print_modtype extent env mp locals mtb = match mtb.mod_type_alg with - | Some me -> print_expression true extent env mp locals me - | None -> print_signature true extent env mp locals mtb.mod_type +and print_modtype ~mod_ops extent env mp locals mtb = match mtb.mod_type_alg with + | Some me -> print_expression ~mod_ops true extent env mp locals me + | None -> print_signature ~mod_ops true extent env mp locals mtb.mod_type let rec printable_body dir = let dir = pop_dirpath dir in @@ -403,52 +408,52 @@ let rec printable_body dir = (** Since we might play with nametab above, we should reset to prior state after the printing *) -let print_expression' is_type extent env mp me = +let print_expression' ~mod_ops is_type extent env mp me = States.with_state_protection - (fun e -> print_expression is_type extent env mp [] e) me + (fun e -> print_expression ~mod_ops is_type extent env mp [] e) me -let print_signature' is_type extent env mp me = +let print_signature' ~mod_ops is_type extent env mp me = States.with_state_protection - (fun e -> print_signature is_type extent env mp [] e) me + (fun e -> print_signature ~mod_ops is_type extent env mp [] e) me -let unsafe_print_module extent env mp with_body mb = +let unsafe_print_module ~mod_ops extent env mp with_body mb = let name = print_modpath [] mp in let pr_equals = spc () ++ str ":= " in let body = match with_body, mb.mod_expr with | false, _ | true, Abstract -> mt() - | _, Algebraic me -> pr_equals ++ print_expression' false extent env mp me - | _, Struct sign -> pr_equals ++ print_signature' false extent env mp sign - | _, FullStruct -> pr_equals ++ print_signature' false extent env mp mb.mod_type + | _, Algebraic me -> pr_equals ++ print_expression' ~mod_ops false extent env mp me + | _, Struct sign -> pr_equals ++ print_signature' ~mod_ops false extent env mp sign + | _, FullStruct -> pr_equals ++ print_signature' ~mod_ops false extent env mp mb.mod_type in let modtype = match mb.mod_expr, mb.mod_type_alg with | FullStruct, _ -> mt () - | _, Some ty -> brk (1,1) ++ str": " ++ print_expression' true extent env mp ty - | _, _ -> brk (1,1) ++ str": " ++ print_signature' true extent env mp mb.mod_type + | _, Some ty -> brk (1,1) ++ str": " ++ print_expression' ~mod_ops true extent env mp ty + | _, _ -> brk (1,1) ++ str": " ++ print_signature' ~mod_ops true extent env mp mb.mod_type in hv 0 (keyword "Module" ++ spc () ++ name ++ modtype ++ body) exception ShortPrinting -let print_module with_body mp = +let print_module ~mod_ops with_body mp = let me = Global.lookup_module mp in try if !short then raise ShortPrinting; - unsafe_print_module WithContents + unsafe_print_module ~mod_ops WithContents (Global.env ()) mp with_body me ++ fnl () with e when CErrors.noncritical e -> - unsafe_print_module OnlyNames + unsafe_print_module ~mod_ops OnlyNames (Global.env ()) mp with_body me ++ fnl () -let print_modtype kn = +let print_modtype ~mod_ops kn = let mtb = Global.lookup_modtype kn in let name = print_kn [] kn in hv 1 (keyword "Module Type" ++ spc () ++ name ++ str " =" ++ spc () ++ try if !short then raise ShortPrinting; - print_signature' true WithContents + print_signature' ~mod_ops true WithContents (Global.env ()) kn mtb.mod_type with e when CErrors.noncritical e -> - print_signature' true OnlyNames + print_signature' ~mod_ops true OnlyNames (Global.env ()) kn mtb.mod_type) diff --git a/printing/printmod.mli b/printing/printmod.mli index 8fd1cb4183..4c9245ee27 100644 --- a/printing/printmod.mli +++ b/printing/printmod.mli @@ -16,5 +16,11 @@ val printable_body : DirPath.t -> bool val pr_mutual_inductive_body : Environ.env -> MutInd.t -> Declarations.mutual_inductive_body -> UnivNames.univ_name_list option -> Pp.t -val print_module : bool -> ModPath.t -> Pp.t -val print_modtype : ModPath.t -> Pp.t + +type mod_ops = + { import_module : export:bool -> ModPath.t -> unit + ; process_module_binding : MBId.t -> Declarations.module_alg_expr -> unit + } + +val print_module : mod_ops:mod_ops -> bool -> ModPath.t -> Pp.t +val print_modtype : mod_ops:mod_ops -> ModPath.t -> Pp.t diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index 7658ad68a5..642dc94ab2 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -54,7 +54,10 @@ let coqc_main copts ~opts = if opts.Coqargs.post.Coqargs.output_context then begin let sigma, env = let e = Global.env () in Evd.from_env e, e in let library_accessor = Library.indirect_accessor in - Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context ~library_accessor env) sigma) ++ fnl ()) + let mod_ops = { Printmod.import_module = Declaremods.import_module + ; process_module_binding = Declaremods.process_module_binding + } in + Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context ~mod_ops ~library_accessor env) sigma) ++ fnl ()) end; CProfile.print_profile () diff --git a/library/declaremods.ml b/vernac/declaremods.ml index b4dc42bdfe..58a7dff5fd 100644 --- a/library/declaremods.ml +++ b/vernac/declaremods.ml @@ -35,8 +35,6 @@ type inline = | DefaultInline | InlineAt of int -type module_kind = Module | ModType | ModAny - let default_inline () = Some (Flags.get_inline_level ()) let inl2intopt = function @@ -457,15 +455,15 @@ let rec compute_subst env mbids sign mp_l inl = | _,[] -> mbids,empty_subst | [],r -> user_err Pp.(str "Application of a functor with too few arguments.") | mbid::mbids,mp::mp_l -> - let farg_id, farg_b, fbody_b = Modops.destr_functor sign in - let mb = Environ.lookup_module mp env in - let mbid_left,subst = compute_subst env mbids fbody_b mp_l inl in - let resolver = + let farg_id, farg_b, fbody_b = Modops.destr_functor sign in + let mb = Environ.lookup_module mp env in + let mbid_left,subst = compute_subst env mbids fbody_b mp_l inl in + let resolver = if Modops.is_functor mb.mod_type then empty_delta_resolver else Modops.inline_delta_resolver env inl mp farg_id farg_b mb.mod_delta - in - mbid_left,join (map_mbid mbid mp resolver) subst + in + mbid_left,join (map_mbid mbid mp resolver) subst (** Create the objects of a "with Module" structure. *) @@ -547,11 +545,11 @@ let process_module_binding mbid me = Objects in these parameters are also loaded. Output is accumulated on top of [acc] (in reverse order). *) -let intern_arg interp_modast (acc, cst) (idl,(typ,ann)) = +let intern_arg (acc, cst) (idl,(typ,ann)) = let inl = inl2intopt ann in let lib_dir = Lib.library_dp() in let env = Global.env() in - let (mty, _, cst') = interp_modast env ModType typ in + let (mty, _, cst') = Modintern.interp_module_ast env Modintern.ModType typ in let () = Global.push_context_set true cst' in let env = Global.env () in let sobjs = get_module_sobjs false env inl mty in @@ -579,8 +577,8 @@ let intern_arg interp_modast (acc, cst) (idl,(typ,ann)) = be more efficient and independent of [List.map] eval order. *) -let intern_args interp_modast params = - List.fold_left (intern_arg interp_modast) ([], Univ.ContextSet.empty) params +let intern_args params = + List.fold_left intern_arg ([], Univ.ContextSet.empty) params (** {6 Auxiliary functions concerning subtyping checks} *) @@ -588,10 +586,10 @@ let intern_args interp_modast params = let check_sub mtb sub_mtb_l = (* The constraints are checked and forgot immediately : *) ignore (List.fold_right - (fun sub_mtb env -> - Environ.add_constraints - (Subtyping.check_subtypes env mtb sub_mtb) env) - sub_mtb_l (Global.env())) + (fun sub_mtb env -> + Environ.add_constraints + (Subtyping.check_subtypes env mtb sub_mtb) env) + sub_mtb_l (Global.env())) (** This function checks if the type calculated for the module [mp] is a subtype of all signatures in [sub_mtb_l]. Uses only the global @@ -631,11 +629,11 @@ let mk_funct_type env args seb0 = (** Prepare the module type list for check of subtypes *) -let build_subtypes interp_modast env mp args mtys = +let build_subtypes env mp args mtys = let (cst, ans) = List.fold_left_map (fun cst (m,ann) -> let inl = inl2intopt ann in - let mte, _, cst' = interp_modast env ModType m in + let mte, _, cst' = Modintern.interp_module_ast env Modintern.ModType m in let env = Environ.push_context_set ~strict:true cst' env in let cst = Univ.ContextSet.union cst cst' in let mtb = Mod_typing.translate_modtype env mp inl ([],mte) in @@ -673,22 +671,22 @@ let openmodtype_info = module RawModOps = struct -let start_module interp_modast export id args res fs = +let start_module export id args res fs = let mp = Global.start_module id in - let arg_entries_r, cst = intern_args interp_modast args in + let arg_entries_r, cst = intern_args args in let () = Global.push_context_set true cst in let env = Global.env () in let res_entry_o, subtyps, cst = match res with | Enforce (res,ann) -> let inl = inl2intopt ann in - let (mte, _, cst) = interp_modast env ModType res in + let (mte, _, cst) = Modintern.interp_module_ast env Modintern.ModType res in let env = Environ.push_context_set ~strict:true cst env in (* We check immediately that mte is well-formed *) let _, _, _, cst' = Mod_typing.translate_mse env None inl mte in let cst = Univ.ContextSet.union cst cst' in Some (mte, inl), [], cst | Check resl -> - let typs, cst = build_subtypes interp_modast env mp arg_entries_r resl in + let typs, cst = build_subtypes env mp arg_entries_r resl in None, typs, cst in let () = Global.push_context_set true cst in @@ -735,25 +733,25 @@ let end_module () = mp -let declare_module interp_modast id args res mexpr_o fs = +let declare_module id args res mexpr_o fs = (* We simulate the beginning of an interactive module, then we adds the module parameters to the global env. *) let mp = Global.start_module id in - let arg_entries_r, cst = intern_args interp_modast args in + let arg_entries_r, cst = intern_args args in let params = mk_params_entry arg_entries_r in let env = Global.env () in let env = Environ.push_context_set ~strict:true cst env in let mty_entry_o, subs, inl_res, cst' = match res with | Enforce (mty,ann) -> let inl = inl2intopt ann in - let (mte, _, cst) = interp_modast env ModType mty in + let (mte, _, cst) = Modintern.interp_module_ast env Modintern.ModType mty in let env = Environ.push_context_set ~strict:true cst env in (* We check immediately that mte is well-formed *) let _, _, _, cst' = Mod_typing.translate_mse env None inl mte in let cst = Univ.ContextSet.union cst cst' in Some mte, [], inl, cst | Check mtys -> - let typs, cst = build_subtypes interp_modast env mp arg_entries_r mtys in + let typs, cst = build_subtypes env mp arg_entries_r mtys in None, typs, default_inline (), cst in let env = Environ.push_context_set ~strict:true cst' env in @@ -761,7 +759,7 @@ let declare_module interp_modast id args res mexpr_o fs = let mexpr_entry_o, inl_expr, cst' = match mexpr_o with | None -> None, default_inline (), Univ.ContextSet.empty | Some (mexpr,ann) -> - let (mte, _, cst) = interp_modast env Module mexpr in + let (mte, _, cst) = Modintern.interp_module_ast env Modintern.Module mexpr in Some mte, inl2intopt ann, cst in let env = Environ.push_context_set ~strict:true cst' env in @@ -803,12 +801,12 @@ end module RawModTypeOps = struct -let start_modtype interp_modast id args mtys fs = +let start_modtype id args mtys fs = let mp = Global.start_modtype id in - let arg_entries_r, cst = intern_args interp_modast args in + let arg_entries_r, cst = intern_args args in let () = Global.push_context_set true cst in let env = Global.env () in - let sub_mty_l, cst = build_subtypes interp_modast env mp arg_entries_r mtys in + let sub_mty_l, cst = build_subtypes env mp arg_entries_r mtys in let () = Global.push_context_set true cst in openmodtype_info := sub_mty_l; let prefix = Lib.start_modtype id mp fs in @@ -831,16 +829,16 @@ let end_modtype () = mp -let declare_modtype interp_modast id args mtys (mty,ann) fs = +let declare_modtype id args mtys (mty,ann) fs = let inl = inl2intopt ann in (* We simulate the beginning of an interactive module, then we adds the module parameters to the global env. *) let mp = Global.start_modtype id in - let arg_entries_r, cst = intern_args interp_modast args in + let arg_entries_r, cst = intern_args args in let () = Global.push_context_set true cst in let params = mk_params_entry arg_entries_r in let env = Global.env () in - let mte, _, cst = interp_modast env ModType mty in + let mte, _, cst = Modintern.interp_module_ast env Modintern.ModType mty in let () = Global.push_context_set true cst in let env = Global.env () in (* We check immediately that mte is well-formed *) @@ -848,7 +846,7 @@ let declare_modtype interp_modast id args mtys (mty,ann) fs = let () = Global.push_context_set true cst in let env = Global.env () in let entry = params, mte in - let sub_mty_l, cst = build_subtypes interp_modast env mp arg_entries_r mtys in + let sub_mty_l, cst = build_subtypes env mp arg_entries_r mtys in let () = Global.push_context_set true cst in let env = Global.env () in let sobjs = get_functor_sobjs false env inl entry in @@ -902,12 +900,12 @@ let type_of_incl env is_mod = function decompose_functor mp_l (type_of_mod mp0 env is_mod) |MEwith _ -> raise NoIncludeSelf -let declare_one_include interp_modast (me_ast,annot) = +let declare_one_include (me_ast,annot) = let env = Global.env() in - let me, kind, cst = interp_modast env ModAny me_ast in + let me, kind, cst = Modintern.interp_module_ast env Modintern.ModAny me_ast in let () = Global.push_context_set true cst in let env = Global.env () in - let is_mod = (kind == Module) in + let is_mod = (kind == Modintern.Module) in let cur_mp = Lib.current_mp () in let inl = inl2intopt annot in let mbids,aobjs = get_module_sobjs is_mod env inl me in @@ -925,8 +923,7 @@ let declare_one_include interp_modast (me_ast,annot) = let aobjs = subst_aobjs subst aobjs in ignore (add_leaf (Lib.current_mod_id ()) (IncludeObject aobjs)) -let declare_include interp me_asts = - List.iter (declare_one_include interp) me_asts +let declare_include me_asts = List.iter declare_one_include me_asts end @@ -942,40 +939,40 @@ let protect_summaries f = let () = Summary.unfreeze_summaries fs in iraise reraise -let start_module interp export id args res = - protect_summaries (RawModOps.start_module interp export id args res) +let start_module export id args res = + protect_summaries (RawModOps.start_module export id args res) let end_module = RawModOps.end_module -let declare_module interp id args mtys me_l = +let declare_module id args mtys me_l = let declare_me fs = match me_l with - | [] -> RawModOps.declare_module interp id args mtys None fs - | [me] -> RawModOps.declare_module interp id args mtys (Some me) fs + | [] -> RawModOps.declare_module id args mtys None fs + | [me] -> RawModOps.declare_module id args mtys (Some me) fs | me_l -> - ignore (RawModOps.start_module interp None id args mtys fs); - RawIncludeOps.declare_include interp me_l; - RawModOps.end_module () + ignore (RawModOps.start_module None id args mtys fs); + RawIncludeOps.declare_include me_l; + RawModOps.end_module () in protect_summaries declare_me -let start_modtype interp id args mtys = - protect_summaries (RawModTypeOps.start_modtype interp id args mtys) +let start_modtype id args mtys = + protect_summaries (RawModTypeOps.start_modtype id args mtys) let end_modtype = RawModTypeOps.end_modtype -let declare_modtype interp id args mtys mty_l = +let declare_modtype id args mtys mty_l = let declare_mt fs = match mty_l with | [] -> assert false - | [mty] -> RawModTypeOps.declare_modtype interp id args mtys mty fs + | [mty] -> RawModTypeOps.declare_modtype id args mtys mty fs | mty_l -> - ignore (RawModTypeOps.start_modtype interp id args mtys fs); - RawIncludeOps.declare_include interp mty_l; - RawModTypeOps.end_modtype () + ignore (RawModTypeOps.start_modtype id args mtys fs); + RawIncludeOps.declare_include mty_l; + RawModTypeOps.end_modtype () in protect_summaries declare_mt -let declare_include interp me_asts = - protect_summaries (fun _ -> RawIncludeOps.declare_include interp me_asts) +let declare_include me_asts = + protect_summaries (fun _ -> RawIncludeOps.declare_include me_asts) (** {6 Libraries} *) @@ -1055,12 +1052,7 @@ let iter_all_segments f = (** {6 Some types used to shorten declaremods.mli} *) -type 'modast module_interpretor = - Environ.env -> module_kind -> 'modast -> - Entries.module_struct_entry * module_kind * Univ.ContextSet.t - -type 'modast module_params = - (lident list * ('modast * inline)) list +type module_params = (lident list * (Constrexpr.module_ast * inline)) list (** {6 Debug} *) diff --git a/library/declaremods.mli b/vernac/declaremods.mli index b7c7cd1dba..ae84704656 100644 --- a/library/declaremods.mli +++ b/vernac/declaremods.mli @@ -29,34 +29,24 @@ type inline = (** Kinds of modules *) -type module_kind = Module | ModType | ModAny +type module_params = (lident list * (Constrexpr.module_ast * inline)) list -type 'modast module_interpretor = - Environ.env -> module_kind -> 'modast -> - Entries.module_struct_entry * module_kind * Univ.ContextSet.t - -type 'modast module_params = - (lident list * ('modast * inline)) list - -(** [declare_module interp_modast id fargs typ exprs] - declares module [id], with structure constructed by [interp_modast] - from functor arguments [fargs], with final type [typ]. - [exprs] is usually of length 1 (Module definition with a concrete - body), but it could also be empty ("Declare Module", with non-empty [typ]), - or multiple (body of the shape M <+ N <+ ...). *) +(** [declare_module id fargs typ exprs] declares module [id], from + functor arguments [fargs], with final type [typ]. [exprs] is + usually of length 1 (Module definition with a concrete body), but + it could also be empty ("Declare Module", with non-empty [typ]), or + multiple (body of the shape M <+ N <+ ...). *) val declare_module : - 'modast module_interpretor -> Id.t -> - 'modast module_params -> - ('modast * inline) module_signature -> - ('modast * inline) list -> ModPath.t + module_params -> + (Constrexpr.module_ast * inline) module_signature -> + (Constrexpr.module_ast * inline) list -> ModPath.t val start_module : - 'modast module_interpretor -> bool option -> Id.t -> - 'modast module_params -> - ('modast * inline) module_signature -> ModPath.t + module_params -> + (Constrexpr.module_ast * inline) module_signature -> ModPath.t val end_module : unit -> ModPath.t @@ -68,18 +58,16 @@ val end_module : unit -> ModPath.t Similar to [declare_module], except that the types could be multiple *) val declare_modtype : - 'modast module_interpretor -> Id.t -> - 'modast module_params -> - ('modast * inline) list -> - ('modast * inline) list -> + module_params -> + (Constrexpr.module_ast * inline) list -> + (Constrexpr.module_ast * inline) list -> ModPath.t val start_modtype : - 'modast module_interpretor -> Id.t -> - 'modast module_params -> - ('modast * inline) list -> ModPath.t + module_params -> + (Constrexpr.module_ast * inline) list -> ModPath.t val end_modtype : unit -> ModPath.t @@ -117,8 +105,7 @@ val import_modules : export:bool -> ModPath.t list -> unit (** Include *) -val declare_include : - 'modast module_interpretor -> ('modast * inline) list -> unit +val declare_include : (Constrexpr.module_ast * inline) list -> unit (** {6 ... } *) (** [iter_all_segments] iterate over all segments, the modules' diff --git a/vernac/himsg.ml b/vernac/himsg.ml index ea34b601e8..c335d3ad55 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1079,9 +1079,7 @@ let explain_incorrect_with_in_module () = let explain_incorrect_module_application () = str "Illegal application to a module type." -open Modintern - -let explain_module_internalization_error = function +let explain_module_internalization_error = let open Modintern in function | NotAModuleNorModtype s -> explain_not_module_nor_modtype s | IncorrectWithInModule -> explain_incorrect_with_in_module () | IncorrectModuleApplication -> explain_incorrect_module_application () diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index cd13f83e96..4868182bb3 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -1,6 +1,7 @@ Vernacexpr Attributes Pvernac +Declaremods G_vernac G_proofs Vernacprop diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 43b58d6d4b..ca29a6afb9 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -872,10 +872,7 @@ let vernac_declare_module export {loc;v=id} binders_ast mty_ast = if not (Option.is_empty export) then user_err Pp.(str "Arguments of a functor declaration cannot be exported. Remove the \"Export\" and \"Import\" keywords from every functor argument.") else (idl,ty)) binders_ast in - let mp = - Declaremods.declare_module Modintern.interp_module_ast - id binders_ast (Declaremods.Enforce mty_ast) [] - in + let mp = Declaremods.declare_module id binders_ast (Declaremods.Enforce mty_ast) [] in Dumpglob.dump_moddef ?loc mp "mod"; Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared"); Option.iter (fun export -> vernac_import export [qualid_of_ident id]) export @@ -892,10 +889,7 @@ let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mt (fun (export,idl,ty) (args,argsexport) -> (idl,ty)::args, (List.map (fun {v=i} -> export,i)idl)@argsexport) binders_ast ([],[]) in - let mp = - Declaremods.start_module Modintern.interp_module_ast - export id binders_ast mty_ast_o - in + let mp = Declaremods.start_module export id binders_ast mty_ast_o in Dumpglob.dump_moddef ?loc mp "mod"; Flags.if_verbose Feedback.msg_info (str "Interactive Module " ++ Id.print id ++ str " started"); @@ -911,7 +905,7 @@ let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mt user_err Pp.(str "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument.") else (idl,ty)) binders_ast in let mp = - Declaremods.declare_module Modintern.interp_module_ast + Declaremods.declare_module id binders_ast mty_ast_o mexpr_ast_l in Dumpglob.dump_moddef ?loc mp "mod"; @@ -938,10 +932,7 @@ let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l = (idl,ty)::args, (List.map (fun {v=i} -> export,i)idl)@argsexport) binders_ast ([],[]) in - let mp = - Declaremods.start_modtype Modintern.interp_module_ast - id binders_ast mty_sign - in + let mp = Declaremods.start_modtype id binders_ast mty_sign in Dumpglob.dump_moddef ?loc mp "modtype"; Flags.if_verbose Feedback.msg_info (str "Interactive Module Type " ++ Id.print id ++ str " started"); @@ -957,10 +948,7 @@ let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l = if not (Option.is_empty export) then user_err Pp.(str "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument.") else (idl,ty)) binders_ast in - let mp = - Declaremods.declare_modtype Modintern.interp_module_ast - id binders_ast mty_sign mty_ast_l - in + let mp = Declaremods.declare_modtype id binders_ast mty_sign mty_ast_l in Dumpglob.dump_moddef ?loc mp "modtype"; Flags.if_verbose Feedback.msg_info (str "Module Type " ++ Id.print id ++ str " is defined") @@ -970,8 +958,7 @@ let vernac_end_modtype {loc;v=id} = Dumpglob.dump_modref ?loc mp "modtype"; Flags.if_verbose Feedback.msg_info (str "Module Type " ++ Id.print id ++ str " is defined") -let vernac_include l = - Declaremods.declare_include Modintern.interp_module_ast l +let vernac_include l = Declaremods.declare_include l (**********************) (* Gallina extensions *) @@ -1966,26 +1953,29 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt = print_about env sigma ref_or_by_not udecl let vernac_print ~pstate ~atts = + let mod_ops = { Printmod.import_module = Declaremods.import_module + ; process_module_binding = Declaremods.process_module_binding + } in let sigma, env = get_current_or_global_context ~pstate in function | PrintTypingFlags -> pr_typing_flags (Environ.typing_flags (Global.env ())) | PrintTables -> print_tables () - | PrintFullContext-> print_full_context_typ Library.indirect_accessor env sigma - | PrintSectionContext qid -> print_sec_context_typ Library.indirect_accessor env sigma qid - | PrintInspect n -> inspect Library.indirect_accessor env sigma n + | PrintFullContext-> print_full_context_typ ~mod_ops Library.indirect_accessor env sigma + | PrintSectionContext qid -> print_sec_context_typ ~mod_ops Library.indirect_accessor env sigma qid + | PrintInspect n -> inspect ~mod_ops Library.indirect_accessor env sigma n | PrintGrammar ent -> Metasyntax.pr_grammar ent | PrintCustomGrammar ent -> Metasyntax.pr_custom_grammar ent | PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir | PrintModules -> print_modules () - | PrintModule qid -> print_module qid - | PrintModuleType qid -> print_modtype qid + | PrintModule qid -> print_module ~mod_ops qid + | PrintModuleType qid -> print_modtype ~mod_ops qid | PrintNamespace ns -> print_namespace ~pstate ns | PrintMLLoadPath -> Mltop.print_ml_path () | PrintMLModules -> Mltop.print_ml_modules () | PrintDebugGC -> Mltop.print_gc () | PrintName (qid,udecl) -> dump_global qid; - print_name Library.indirect_accessor env sigma qid udecl + print_name ~mod_ops Library.indirect_accessor env sigma qid udecl | PrintGraph -> Prettyp.print_graph () | PrintClasses -> Prettyp.print_classes() | PrintTypeClasses -> Prettyp.print_typeclasses() |