Skip to content

Commit e32de1a

Browse files
SkySkimmerlukaszcz
authored andcommitted
Adapt to rocq-prover/rocq#20371 (dirpath_of_module -> path_of_module, returning full_path)
1 parent c405d3f commit e32de1a

File tree

2 files changed

+2
-2
lines changed

2 files changed

+2
-2
lines changed

src/lib/hhutils.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ let exists_global s =
3030
let match_globref m g =
3131
let (p2, id2) = Libnames.repr_path (Nametab.path_of_global g)
3232
in
33-
let l1 = List.rev @@ Names.DirPath.repr (Nametab.dirpath_of_module m)
33+
let l1 = List.rev @@ Names.DirPath.repr (Libnames.dirpath_of_path @@ Nametab.path_of_module m)
3434
and l2 = List.rev @@ id2 :: Names.DirPath.repr p2
3535
in
3636
let rec pom l1 l2 =

src/plugin/opt.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -259,7 +259,7 @@ module HammerFilter = struct
259259
let check_local _ _ = ()
260260
let discharge x = x
261261
let subst = Mod_subst.subst_mp
262-
let printer m = Names.DirPath.print (Nametab.dirpath_of_module m)
262+
let printer m = Libnames.pr_path (Nametab.path_of_module m)
263263
let key = ["Hammer"; "Filter"]
264264
let title = "Hammer Filter"
265265
let member_message m b =

0 commit comments

Comments
 (0)