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 561b0078a..13ed65056 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -231,7 +231,7 @@ let add_glob ?loc ref = add_glob_gen ?loc sp lib_dp ty let mp_of_kn kn = - let mp,sec,l = Names.repr_kn kn in + let mp,sec,l = Names.KerName.repr kn in Names.MPdot (mp,l) let add_glob_kn ?loc kn = |