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/declaremods.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/declaremods.mli')
| -rw-r--r-- | vernac/declaremods.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/vernac/declaremods.mli b/vernac/declaremods.mli index 5e45957e83..9ca2ca5593 100644 --- a/vernac/declaremods.mli +++ b/vernac/declaremods.mli @@ -126,5 +126,3 @@ val debug_print_modtab : unit -> Pp.t val process_module_binding : MBId.t -> Declarations.module_alg_expr -> unit - -val mod_ops : Printmod.mod_ops |