Skip to content

Commit 41b7f87

Browse files
committed
Adapt to rocq-prover/rocq#20642 (rm SyntacticOrd)
1 parent 53b0779 commit 41b7f87

File tree

1 file changed

+1
-5
lines changed

1 file changed

+1
-5
lines changed

src/rocq_elpi_HOAS.ml

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -622,11 +622,7 @@ module GRSet = U.Set.Make(GROrd)
622622
let globalc = E.Constants.declare_global_symbol "global"
623623
let pglobalc = E.Constants.declare_global_symbol "pglobal"
624624

625-
module GrefCache = Hashtbl.Make(struct
626-
type t = GlobRef.t
627-
let equal = GlobRef.SyntacticOrd.equal
628-
let hash = GlobRef.SyntacticOrd.hash
629-
end)
625+
module GrefCache = Hashtbl.Make(GlobRef.UserOrd)
630626
let cache = GrefCache.create 13
631627

632628
let assert_in_coq_gref_consistent ~poly gr =

0 commit comments

Comments
 (0)