diff options
Diffstat (limited to 'plugins/extraction/table.ml')
| -rw-r--r-- | plugins/extraction/table.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 1fd4840fe..2dd07b2f2 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -67,7 +67,7 @@ let is_toplevel mp = let at_toplevel mp = is_modfile mp || is_toplevel mp -let rec mp_length mp = +let mp_length mp = let mp0 = current_toplevel () in let rec len = function | mp when mp = mp0 -> 1 |