diff options
| author | Gaëtan Gilbert | 2019-10-31 14:55:05 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-10-31 17:06:15 +0100 |
| commit | 85905b38c15c3d2bb73e878e6e7db180b73d468e (patch) | |
| tree | 715c6f35f099b48aa1c1540d2f53d958b35fe230 /vernac/declaremods.mli | |
| parent | 777109f0068d524ca2a82d405416da273fec3d7f (diff) | |
[prettyp] remove `mod_ops` and `indirect_accessor` parameters
`Prettyp` is now late enough in linking to refer to them.
Diffstat (limited to 'vernac/declaremods.mli')
| -rw-r--r-- | vernac/declaremods.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/vernac/declaremods.mli b/vernac/declaremods.mli index ae84704656..23f25bc597 100644 --- a/vernac/declaremods.mli +++ b/vernac/declaremods.mli @@ -126,3 +126,5 @@ val debug_print_modtab : unit -> Pp.t val process_module_binding : MBId.t -> Declarations.module_alg_expr -> unit + +val mod_ops : Printmod.mod_ops |