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]