diff options
Diffstat (limited to 'src/tac2entries.ml')
| -rw-r--r-- | src/tac2entries.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/tac2entries.ml b/src/tac2entries.ml index c26fbdc478..2936f143ce 100644 --- a/src/tac2entries.ml +++ b/src/tac2entries.ml @@ -100,8 +100,8 @@ type typdef = { } let change_kn_label kn id = - let (mp, dp, _) = KerName.repr kn in - KerName.make mp dp (Label.of_id id) + let mp = KerName.modpath kn in + KerName.make mp (Label.of_id id) let change_sp_label sp id = let (dp, _) = Libnames.repr_path sp in |