diff options
| -rw-r--r-- | contrib/extraction/common.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml index c71edf5102..09a58648ea 100644 --- a/contrib/extraction/common.ml +++ b/contrib/extraction/common.ml @@ -259,7 +259,7 @@ module StdParams = struct else short in add_module_contents mp s; (* update the visible environment *) - str s + str final let pp_long_module mpl mp = try (* has [mp] something in common with one of those in [mpl] ? *) |