diff options
Diffstat (limited to 'interp/dumpglob.ml')
| -rw-r--r-- | interp/dumpglob.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index ccad6b19eb..f5be0ddbae 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -234,7 +234,7 @@ let add_glob ?loc ref = add_glob_gen ?loc sp lib_dp ty let mp_of_kn kn = - let mp,sec,l = Names.KerName.repr kn in + let mp,l = Names.KerName.repr kn in Names.MPdot (mp,l) let add_glob_kn ?loc kn = |