Skip to content

Commit eca8630

Browse files
SkySkimmerlukaszcz
authored andcommitted
Adapt to rocq-prover/rocq#19390 (goptions tables can discharge) + fix module substitution
1 parent 7dcbc6a commit eca8630

File tree

1 file changed

+3
-1
lines changed

1 file changed

+3
-1
lines changed

src/plugin/opt.ml

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -256,7 +256,9 @@ module HammerFilter = struct
256256
type t = Names.ModPath.t
257257
module Set = FilterSet
258258
let encode env = Nametab.locate_module
259-
let subst s m = m
259+
let check_local _ _ = ()
260+
let discharge x = x
261+
let subst = Mod_subst.subst_mp
260262
let printer m = Names.DirPath.print (Nametab.dirpath_of_module m)
261263
let key = ["Hammer"; "Filter"]
262264
let title = "Hammer Filter"

0 commit comments

Comments
 (0)