diff options
| author | Maxime Dénès | 2018-09-26 16:20:07 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-26 16:20:07 +0200 |
| commit | 118a93ccf954d02afbfa5ef2b3735ef37439b274 (patch) | |
| tree | cf9d5ba237d1fcdf18aaca6b2d880a6cd96e365f | |
| parent | ccb701d78394a108daf25e62d40ba059aa3fce62 (diff) | |
Adapt to removal of section paths from kernel names
| -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 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 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 ")") |