Adapt to coq/coq#20178 (inductive_arity doesn't exist)

ejgallego · Feb 5, 2025 · e8e43f2 · e8e43f2
1 parent 76479da
commit e8e43f2
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 29 deletions.
diff --git a/serlib/ser_declarations.ml b/serlib/ser_declarations.ml
@@ -40,10 +40,6 @@ module Float64 = Ser_float64
 module Pstring = Ser_pstring
 module Vmlibrary = Ser_vmlibrary
 
-type template_arity =
-  [%import: Declarations.template_arity]
-  [@@deriving sexp,yojson,hash,compare]
-
 type recarg_type =
   [%import: Declarations.recarg_type]
   [@@deriving sexp,yojson,hash,compare]
@@ -56,15 +52,6 @@ type wf_paths =
   [%import: Declarations.wf_paths]
   [@@deriving sexp,yojson,hash,compare]
 
-type regular_inductive_arity =
-  [%import: Declarations.regular_inductive_arity
-  [@with Term.sorts := Sorts.t;]]
-  [@@deriving sexp,yojson,hash,compare]
-
-type inductive_arity =
-  [%import: Declarations.inductive_arity]
-  [@@deriving sexp,yojson,hash,compare]
-
 type squash_info =
   [%import: Declarations.squash_info]
   [@@deriving sexp,yojson,hash,compare]
@@ -143,10 +130,6 @@ type record_info =
   [%import: Declarations.record_info]
   [@@deriving sexp,yojson,hash,compare]
 
-type template_pseudo_sort_poly =
-  [%import: Declarations.template_pseudo_sort_poly]
-  [@@deriving sexp,yojson,hash,compare]
-
 type template_universes =
   [%import: Declarations.template_universes]
   [@@deriving sexp,yojson,hash,compare]

diff --git a/serlib/ser_declarations.mli b/serlib/ser_declarations.mli
@@ -16,24 +16,12 @@
 (* Written by: Emilio J. Gallego Arias and others                       *)
 (************************************************************************)
 
-open Sexplib
-
-type template_arity = Declarations.template_arity
-val template_arity_of_sexp : Sexp.t -> template_arity
-val sexp_of_template_arity : template_arity -> Sexp.t
-
 type recarg = Declarations.recarg
   [@@deriving sexp,yojson,hash,compare]
 
 type wf_paths = recarg Rtree.t
   [@@deriving sexp,yojson,hash,compare]
 
-type regular_inductive_arity = Declarations.regular_inductive_arity
-  [@@deriving sexp,yojson,hash,compare]
-
-type inductive_arity = Declarations.inductive_arity
-  [@@deriving sexp,yojson,hash,compare]
-
 type one_inductive_body = Declarations.one_inductive_body
   [@@deriving sexp,yojson,hash,compare]