From b8dfcedf39f8930b3e081e1d7117a1d58a935ebf Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <herbelin@users.noreply.github.com>
Date: Wed, 19 Jun 2024 18:32:22 +0200
Subject: [PATCH] Adapt to Coq PR #19075: make CSet extensible (#378)

Co-authored-by: Yishuai Li <liyishuai.lys@alibaba-inc.com>
---
 plugin/dune                              | 4 ++++
 plugin/{unifyQC.mli => unifyQC.mli.cppo} | 8 ++++++++
 2 files changed, 12 insertions(+)
 rename plugin/{unifyQC.mli => unifyQC.mli.cppo} (95%)

diff --git a/plugin/dune b/plugin/dune
index 28e454093..9a7784e3e 100644
--- 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 b/plugin/unifyQC.mli.cppo
similarity index 95%
rename from plugin/unifyQC.mli
rename to plugin/unifyQC.mli.cppo
index 83c7d88d4..22718047a 100644
--- a/plugin/unifyQC.mli
+++ b/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 :