Adapt to Coq PR #19075: make CSet extensible (QuickChick#378)

Co-authored-by: Yishuai Li <[email protected]>
proux01 · Jun 19, 2024 · b8dfced · b8dfced
1 parent b7c8bb7
commit b8dfced
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 0 deletions.
diff --git a/plugin/dune b/plugin/dune
@@ -59,6 +59,10 @@
   (alias compat)
   (target unifyQC.ml)
   (action (run %{exe:../scripts/mycppo} %{dep:unifyQC.ml.cppo} %{target})))
+(rule
+  (alias compat)
+  (target unifyQC.mli)
+  (action (run %{exe:../scripts/mycppo} %{dep:unifyQC.mli.cppo} %{target})))
 (rule
   (alias compat)
   (target weightmap.mlg)

diff --git a/plugin/unifyQC.mli → plugin/unifyQC.mli.cppo b/plugin/unifyQC.mli → plugin/unifyQC.mli.cppo
@@ -30,11 +30,19 @@ val umfind : UM.key -> 'a UM.t -> 'a
 val lookup : unknown -> umap -> range option
 module OrdTSS :
   sig type t = unknown * unknown val compare : 'a -> 'a -> int end
+#if COQ_VERSION >= (8, 20, 0)
+module EqSet : CSet.ExtS with type elt = OrdTSS.t
+#else
 module EqSet : Set.S with type elt = OrdTSS.t
+#endif
 val eq_set_add : unknown -> unknown -> EqSet.t -> EqSet.t
 module OrdTyp :
   sig type t = GenericLib.dep_type val compare : 'a -> 'a -> int end
+#if COQ_VERSION >= (8, 20, 0)
+module ArbSet : CSet.ExtS with type elt = OrdTyp.t
+#else
 module ArbSet : Set.S with type elt = OrdTyp.t
+#endif
 type unknown_provider = { next_unknown : unit -> Unknown.t; }
 val unk_provider : unknown_provider
 val raiseMatch :