From e8e43f26d526646f674c528fe0a6312a2b90536f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 5 Feb 2025 14:05:52 +0100 Subject: [PATCH] Adapt to coq/coq#20178 (inductive_arity doesn't exist) --- serlib/ser_declarations.ml | 17 ----------------- serlib/ser_declarations.mli | 12 ------------ 2 files changed, 29 deletions(-) diff --git a/serlib/ser_declarations.ml b/serlib/ser_declarations.ml index f2d11dd1..89aaa968 100644 --- 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 index e4050642..584b8c90 100644 --- 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]