Skip to content

Commit

Permalink
Adapt to coq/coq#18331 (sort poly inductives)
Browse files Browse the repository at this point in the history
  • Loading branch information
SkySkimmer committed Nov 27, 2023
1 parent 307889d commit b3b3d8b
Show file tree
Hide file tree
Showing 5 changed files with 12 additions and 1 deletion.
4 changes: 4 additions & 0 deletions serlib/ser_declarations.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
1 change: 1 addition & 0 deletions serlib/ser_names.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
1 change: 1 addition & 0 deletions serlib/ser_names.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
6 changes: 5 additions & 1 deletion serlib/ser_sorts.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions serlib/ser_sorts.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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

0 comments on commit b3b3d8b

Please sign in to comment.