diff options
Diffstat (limited to 'printing/printmod.ml')
| -rw-r--r-- | printing/printmod.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/printmod.ml b/printing/printmod.ml index 88880c293..ee4a2db7f 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -116,7 +116,7 @@ let nametab_register_module_body mp struc = let nametab_register_module_param mbid seb = (* For algebraic seb, we use a Declaremods function that converts into mse *) - try Declaremods.process_module_seb_binding mbid seb + try Declaremods.process_module_binding mbid seb with e when Errors.noncritical e -> (* Otherwise, for expanded structure, we try to play with the nametab *) match seb with |