Adapt to coq/coq#19390 (goptions tables can discharge) + fix module s…

…ubstitution
lukaszcz · Jul 28, 2024 · eca8630 · eca8630
1 parent 7dcbc6a
commit eca8630
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/src/plugin/opt.ml b/src/plugin/opt.ml
@@ -256,7 +256,9 @@ module HammerFilter = struct
   type t = Names.ModPath.t
   module Set = FilterSet
   let encode env = Nametab.locate_module
-  let subst s m = m
+  let check_local _ _ = ()
+  let discharge x = x
+  let subst = Mod_subst.subst_mp
   let printer m = Names.DirPath.print (Nametab.dirpath_of_module m)
   let key = ["Hammer"; "Filter"]
   let title = "Hammer Filter"