diff options
| author | Pierre-Marie Pédrot | 2018-10-06 17:09:19 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-06 17:09:19 +0200 |
| commit | 0d46f9a60891829710210fe114171c2e80e43b64 (patch) | |
| tree | ae03691500b173086b6ca674129c3f6e3d7eae45 /src | |
| parent | 0579efd93eebb18f94c90718b092ae4b68a2262d (diff) | |
| parent | 118a93ccf954d02afbfa5ef2b3735ef37439b274 (diff) | |
Merge remote-tracking branch 'maximedenes/rm-section-path'
Diffstat (limited to 'src')
| -rw-r--r-- | src/tac2entries.ml | 4 | ||||
| -rw-r--r-- | src/tac2print.ml | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/src/tac2entries.ml b/src/tac2entries.ml index 95a5f954c6..ec10dea777 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 diff --git a/src/tac2print.ml b/src/tac2print.ml index 9c530dfc51..0fea07ee3a 100644 --- a/src/tac2print.ml +++ b/src/tac2print.ml @@ -16,8 +16,8 @@ open Tac2ffi (** Utils *) 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 paren p = hov 2 (str "(" ++ p ++ str ")") |