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/vernacentries.ml | |
| 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/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index d44e4babf4..f5ef5ee86f 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -175,7 +175,7 @@ let print_module qid = let globdir = Nametab.locate_dir qid in match globdir with DirModule Nametab.{ obj_dir; obj_mp; _ } -> - Printmod.print_module ~mod_ops:Declaremods.mod_ops (Printmod.printable_body obj_dir) obj_mp + Printmod.print_module (Printmod.printable_body obj_dir) obj_mp | _ -> raise Not_found with Not_found -> user_err (str"Unknown Module " ++ pr_qualid qid) @@ -183,12 +183,12 @@ let print_module qid = let print_modtype qid = try let kn = Nametab.locate_modtype qid in - Printmod.print_modtype ~mod_ops:Declaremods.mod_ops kn + Printmod.print_modtype kn with Not_found -> (* Is there a module of this name ? If yes we display its type *) try let mp = Nametab.locate_module qid in - Printmod.print_module ~mod_ops:Declaremods.mod_ops false mp + Printmod.print_module false mp with Not_found -> user_err (str"Unknown Module Type or Module " ++ pr_qualid qid) |