From b3b3d8b2fceca5fc47859798c7c407261dce9ae3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Mon, 27 Nov 2023 10:59:19 +0100
Subject: [PATCH] Adapt to coq/coq#18331 (sort poly inductives)

---
 serlib/ser_declarations.ml | 4 ++++
 serlib/ser_names.ml        | 1 +
 serlib/ser_names.mli       | 1 +
 serlib/ser_sorts.ml        | 6 +++++-
 serlib/ser_sorts.mli       | 1 +
 5 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/serlib/ser_declarations.ml b/serlib/ser_declarations.ml
index 114c4519..7fb58c3e 100644
--- a/serlib/ser_declarations.ml
+++ b/serlib/ser_declarations.ml
@@ -63,6 +63,10 @@ type inductive_arity =
   [%import: Declarations.inductive_arity]
   [@@deriving sexp,yojson,hash,compare]
 
+type squash_info =
+  [%import: Declarations.squash_info]
+  [@@deriving sexp,yojson,hash,compare]
+
 type one_inductive_body =
   [%import: Declarations.one_inductive_body]
   [@@deriving sexp,yojson,hash,compare]
diff --git a/serlib/ser_names.ml b/serlib/ser_names.ml
index a46a7ddf..82d2e70a 100644
--- a/serlib/ser_names.ml
+++ b/serlib/ser_names.ml
@@ -218,6 +218,7 @@ module Ind = struct
 end
 
 module Indset_env = Ser_cSet.Make(Indset_env)(Ind)
+module Indmap_env = Ser_cMap.Make(Indmap_env)(Ind)
 
 type inductive =
   [%import: Names.inductive]
diff --git a/serlib/ser_names.mli b/serlib/ser_names.mli
index ba717c10..5fc08930 100644
--- a/serlib/ser_names.mli
+++ b/serlib/ser_names.mli
@@ -51,6 +51,7 @@ module Mindmap : Ser_cMap.ExtS with type key = MutInd.t and type 'a t = 'a Mindm
 module Mindmap_env : Ser_cMap.ExtS with type key = MutInd.t and type 'a t = 'a Mindmap_env.t
 
 module Indset_env : Ser_cSet.ExtS with type elt = inductive and type t = Indset_env.t
+module Indmap_env : Ser_cMap.ExtS with type key = inductive and type 'a t = 'a Indmap_env.t
 
 type 'a tableKey = 'a Names.tableKey
 
diff --git a/serlib/ser_sorts.ml b/serlib/ser_sorts.ml
index ec0f5681..4a0a5f07 100644
--- a/serlib/ser_sorts.ml
+++ b/serlib/ser_sorts.ml
@@ -38,7 +38,11 @@ end
 
 module Quality = struct
   type constant = [%import: Sorts.Quality.constant] [@@deriving sexp,yojson,hash,compare]
-  type t = [%import: Sorts.Quality.t] [@@deriving sexp,yojson,hash,compare]
+  module Self = struct
+    type t = [%import: Sorts.Quality.t] [@@deriving sexp,yojson,hash,compare]
+  end
+  include Self
+  module Set = Ser_cSet.Make(Sorts.Quality.Set)(Self)
 end
 
 module PierceSpec = struct
diff --git a/serlib/ser_sorts.mli b/serlib/ser_sorts.mli
index f3396735..dbae2f9e 100644
--- a/serlib/ser_sorts.mli
+++ b/serlib/ser_sorts.mli
@@ -27,6 +27,7 @@ module Quality : sig
   type constant = Sorts.Quality.constant [@@deriving sexp,yojson,hash,compare]
 
   include SerType.SJHC with type t = Sorts.Quality.t
+  module Set : SerType.SJHC with type t = Sorts.Quality.Set.t
 end
 
 module QConstraints : SerType.SJHC with type t = Sorts.QConstraints.t