coq-serapi 8.20.0+0.20.0 (latest)

module Stateid = Ser_stateid

module Future = Ser_future

module Names = Ser_names

module Univ = Ser_univ

module UVars = Ser_uvars

module Constr = Ser_constr

module Declarations = Ser_declarations

module CPrimitives = Ser_cPrimitives

type universes_entry = Entries.universes_entry =

| Monomorphic_entry
| Polymorphic_entry of UVars.UContext.t

val universes_entry_of_sexp : Sexplib0.Sexp.t -> universes_entry

val sexp_of_universes_entry : universes_entry -> Sexplib0.Sexp.t

type 'a in_universes_entry = 'a * universes_entry

val in_universes_entry_of_sexp : 
  'a. (Sexplib0.Sexp.t -> 'a) ->
  Sexplib0.Sexp.t ->
  'a in_universes_entry

val sexp_of_in_universes_entry : 
  'a. ('a -> Sexplib0.Sexp.t) ->
  'a in_universes_entry ->
  Sexplib0.Sexp.t

type one_inductive_entry = Entries.one_inductive_entry = {

mind_entry_typename : Names.Id.t;
mind_entry_arity : Constr.constr;
mind_entry_consnames : Names.Id.t list;
mind_entry_lc : Constr.constr list;

}

val one_inductive_entry_of_sexp : Sexplib0.Sexp.t -> one_inductive_entry

val sexp_of_one_inductive_entry : one_inductive_entry -> Sexplib0.Sexp.t

type variance_entry = UVars.Variance.t option array

val variance_entry_of_sexp : Sexplib0.Sexp.t -> variance_entry

val sexp_of_variance_entry : variance_entry -> Sexplib0.Sexp.t

type 'a proof_output = Constr.constr Univ.in_universe_context_set * 'a

val proof_output_of_sexp : 
  'a. (Sexplib0.Sexp.t -> 'a) ->
  Sexplib0.Sexp.t ->
  'a proof_output

val sexp_of_proof_output : 
  'a. ('a -> Sexplib0.Sexp.t) ->
  'a proof_output ->
  Sexplib0.Sexp.t

type definition_entry = Entries.definition_entry = {

const_entry_body : Constr.constr;
const_entry_secctx : Names.Id.Set.t option;
const_entry_type : Constr.types option;
const_entry_universes : universes_entry;
const_entry_inline_code : bool;

}

val definition_entry_of_sexp : Sexplib0.Sexp.t -> definition_entry

val sexp_of_definition_entry : definition_entry -> Sexplib0.Sexp.t

type section_def_entry = Entries.section_def_entry = {

secdef_body : Constr.constr;
secdef_type : Constr.types option;

}

val section_def_entry_of_sexp : Sexplib0.Sexp.t -> section_def_entry

val sexp_of_section_def_entry : section_def_entry -> Sexplib0.Sexp.t

type inline = int option

val inline_of_sexp : Sexplib0.Sexp.t -> inline

val sexp_of_inline : inline -> Sexplib0.Sexp.t

type 'a opaque_entry = 'a Entries.opaque_entry = {

opaque_entry_body : 'a;
opaque_entry_secctx : Names.Id.Set.t;
opaque_entry_type : Constr.types;
opaque_entry_universes : universes_entry;

}

val opaque_entry_of_sexp : 
  'a. (Sexplib0.Sexp.t -> 'a) ->
  Sexplib0.Sexp.t ->
  'a opaque_entry

val sexp_of_opaque_entry : 
  'a. ('a -> Sexplib0.Sexp.t) ->
  'a opaque_entry ->
  Sexplib0.Sexp.t

type parameter_entry = Entries.parameter_entry = {

parameter_entry_secctx : Names.Id.Set.t option;
parameter_entry_type : Constr.types;
parameter_entry_universes : universes_entry;
parameter_entry_inline_code : inline;

}

val parameter_entry_of_sexp : Sexplib0.Sexp.t -> parameter_entry

val sexp_of_parameter_entry : parameter_entry -> Sexplib0.Sexp.t

type primitive_entry = Entries.primitive_entry = {

prim_entry_type : Constr.types in_universes_entry option;
prim_entry_content : CPrimitives.op_or_type;

}

val primitive_entry_of_sexp : Sexplib0.Sexp.t -> primitive_entry

val sexp_of_primitive_entry : primitive_entry -> Sexplib0.Sexp.t

type symbol_entry = Entries.symbol_entry = {

symb_entry_type : Constr.types;
symb_entry_unfold_fix : bool;
symb_entry_universes : universes_entry;

}

val symbol_entry_of_sexp : Sexplib0.Sexp.t -> symbol_entry

val sexp_of_symbol_entry : symbol_entry -> Sexplib0.Sexp.t

type constant_entry = Entries.constant_entry =

| DefinitionEntry : definition_entry -> constant_entry
| ParameterEntry : parameter_entry -> constant_entry
| PrimitiveEntry : primitive_entry -> constant_entry
| SymbolEntry : symbol_entry -> constant_entry

val constant_entry_of_sexp : Sexplib0.Sexp.t -> constant_entry

val sexp_of_constant_entry : constant_entry -> Sexplib0.Sexp.t

type module_struct_entry =
  (Constr.constr * UVars.AbstractContext.t option) Declarations.module_alg_expr

val module_struct_entry_of_sexp : Sexplib0.Sexp.t -> module_struct_entry

val sexp_of_module_struct_entry : module_struct_entry -> Sexplib0.Sexp.t

type module_params_entry = (Names.MBId.t * module_struct_entry * inline) list

val module_params_entry_of_sexp : Sexplib0.Sexp.t -> module_params_entry

val sexp_of_module_params_entry : module_params_entry -> Sexplib0.Sexp.t

type module_entry = Entries.module_entry =

| MType of module_params_entry * module_struct_entry
| MExpr of module_params_entry * module_struct_entry * module_struct_entry option

val module_entry_of_sexp : Sexplib0.Sexp.t -> module_entry

val sexp_of_module_entry : module_entry -> Sexplib0.Sexp.t

type module_type_entry = module_params_entry * module_struct_entry

val module_type_entry_of_sexp : Sexplib0.Sexp.t -> module_type_entry

val sexp_of_module_type_entry : module_type_entry -> Sexplib0.Sexp.t

package coq-serapi