diff options
| author | Emilio Jesus Gallego Arias | 2020-06-17 16:02:44 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-30 13:12:01 +0200 |
| commit | b0169fc220ced87d094177575c0dae76d8d87a50 (patch) | |
| tree | bf7370df0dd85436f11eeaa806693472fe8d046a /vernac/printmod.mli | |
| parent | e260c203fa74a587bd78b2803c8ee046ff3df20a (diff) | |
[declaremods] Remove abstraction of imperative module operations
Now that `Printmods` is above `Declaremods`, we don't need to pass the
extra `mod_ops` argument.
Diffstat (limited to 'vernac/printmod.mli')
| -rw-r--r-- | vernac/printmod.mli | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/vernac/printmod.mli b/vernac/printmod.mli index c7f056063b..694821a2d6 100644 --- a/vernac/printmod.mli +++ b/vernac/printmod.mli @@ -17,10 +17,5 @@ val pr_mutual_inductive_body : Environ.env -> MutInd.t -> Declarations.mutual_inductive_body -> UnivNames.univ_name_list option -> 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 +val print_module : bool -> ModPath.t -> Pp.t +val print_modtype : ModPath.t -> Pp.t |