Merge pull request #374 from SkySkimmer/sort-poly-ind

Adapt to coq/coq#18331 (sort poly inductives)

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]

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]

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
 

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

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