coq-serapi 8.12.0+0.12.0 · OCaml Package

type class_rawexpr = Vernacexpr.class_rawexpr

val class_rawexpr_of_sexp : Sexplib.Sexp.t -> class_rawexpr

val sexp_of_class_rawexpr : class_rawexpr -> Sexplib.Sexp.t

type goal_identifier = Vernacexpr.goal_identifier

val goal_identifier_of_sexp : Sexplib.Sexp.t -> goal_identifier

val sexp_of_goal_identifier : goal_identifier -> Sexplib.Sexp.t

type scope_name = Vernacexpr.scope_name

val scope_name_of_sexp : Sexplib.Sexp.t -> scope_name

val sexp_of_scope_name : scope_name -> Sexplib.Sexp.t

type goal_reference = Vernacexpr.goal_reference

val goal_reference_of_sexp : Sexplib.Sexp.t -> goal_reference

val sexp_of_goal_reference : goal_reference -> Sexplib.Sexp.t

type printable = Vernacexpr.printable

val printable_of_sexp : Sexplib.Sexp.t -> printable

val sexp_of_printable : printable -> Sexplib.Sexp.t

type search_item = Vernacexpr.search_item

val search_item_of_sexp : Sexplib.Sexp.t -> search_item

val sexp_of_search_item : search_item -> Sexplib.Sexp.t

type searchable = Vernacexpr.searchable

val searchable_of_sexp : Sexplib.Sexp.t -> searchable

val sexp_of_searchable : searchable -> Sexplib.Sexp.t

type locatable = Vernacexpr.locatable

val locatable_of_sexp : Sexplib.Sexp.t -> locatable

val sexp_of_locatable : locatable -> Sexplib.Sexp.t

type showable = Vernacexpr.showable

val showable_of_sexp : Sexplib.Sexp.t -> showable

val sexp_of_showable : showable -> Sexplib.Sexp.t

type comment = Vernacexpr.comment

val comment_of_sexp : Sexplib.Sexp.t -> comment

val sexp_of_comment : comment -> Sexplib.Sexp.t

type search_restriction = Vernacexpr.search_restriction

val search_restriction_of_sexp : Sexplib.Sexp.t -> search_restriction

val sexp_of_search_restriction : search_restriction -> Sexplib.Sexp.t

type verbose_flag = Vernacexpr.verbose_flag

val verbose_flag_of_sexp : Sexplib.Sexp.t -> verbose_flag

val sexp_of_verbose_flag : verbose_flag -> Sexplib.Sexp.t

type coercion_flag = Vernacexpr.coercion_flag

val coercion_flag_of_sexp : Sexplib.Sexp.t -> coercion_flag

val sexp_of_coercion_flag : coercion_flag -> Sexplib.Sexp.t

type instance_flag = Vernacexpr.instance_flag

val instance_flag_of_sexp : Sexplib.Sexp.t -> instance_flag

val sexp_of_instance_flag : instance_flag -> Sexplib.Sexp.t

type export_flag = Vernacexpr.export_flag

val export_flag_of_sexp : Sexplib.Sexp.t -> export_flag

val sexp_of_export_flag : export_flag -> Sexplib.Sexp.t

type onlyparsing_flag = Vernacexpr.onlyparsing_flag

val onlyparsing_flag_of_sexp : Sexplib.Sexp.t -> onlyparsing_flag

val sexp_of_onlyparsing_flag : onlyparsing_flag -> Sexplib.Sexp.t

type locality_flag = Vernacexpr.locality_flag

val locality_flag_of_sexp : Sexplib.Sexp.t -> locality_flag

val sexp_of_locality_flag : locality_flag -> Sexplib.Sexp.t

type sort_expr = Vernacexpr.sort_expr

val sort_expr_of_sexp : Sexplib.Sexp.t -> sort_expr

val sexp_of_sort_expr : sort_expr -> Sexplib.Sexp.t

type definition_expr = Vernacexpr.definition_expr

val definition_expr_of_sexp : Sexplib.Sexp.t -> definition_expr

val sexp_of_definition_expr : definition_expr -> Sexplib.Sexp.t

type fixpoint_expr = Vernacexpr.fixpoint_expr

val fixpoint_expr_of_sexp : Sexplib.Sexp.t -> fixpoint_expr

val sexp_of_fixpoint_expr : fixpoint_expr -> Sexplib.Sexp.t

type cofixpoint_expr = Vernacexpr.cofixpoint_expr

val cofixpoint_expr_of_sexp : Sexplib.Sexp.t -> cofixpoint_expr

val sexp_of_cofixpoint_expr : cofixpoint_expr -> Sexplib.Sexp.t

type local_decl_expr = Vernacexpr.local_decl_expr

val local_decl_expr_of_sexp : Sexplib.Sexp.t -> local_decl_expr

val sexp_of_local_decl_expr : local_decl_expr -> Sexplib.Sexp.t

type inductive_kind = Vernacexpr.inductive_kind

val inductive_kind_of_sexp : Sexplib.Sexp.t -> inductive_kind

val sexp_of_inductive_kind : inductive_kind -> Sexplib.Sexp.t

type decl_notation = Vernacexpr.decl_notation

val decl_notation_of_sexp : Sexplib.Sexp.t -> decl_notation

val sexp_of_decl_notation : decl_notation -> Sexplib.Sexp.t

type simple_binder = Vernacexpr.simple_binder

val simple_binder_of_sexp : Sexplib.Sexp.t -> simple_binder

val sexp_of_simple_binder : simple_binder -> Sexplib.Sexp.t

type class_binder = Vernacexpr.class_binder

val class_binder_of_sexp : Sexplib.Sexp.t -> class_binder

val sexp_of_class_binder : class_binder -> Sexplib.Sexp.t

type 'a with_coercion = 'a Vernacexpr.with_coercion

val with_coercion_of_sexp : 
  (Sexplib.Sexp.t -> 'a) ->
  Sexplib.Sexp.t ->
  'a with_coercion

val sexp_of_with_coercion : 
  ('a -> Sexplib.Sexp.t) ->
  'a with_coercion ->
  Sexplib.Sexp.t

type constructor_expr = Vernacexpr.constructor_expr

val constructor_expr_of_sexp : Sexplib.Sexp.t -> constructor_expr

val sexp_of_constructor_expr : constructor_expr -> Sexplib.Sexp.t

type constructor_list_or_record_decl_expr =
  Vernacexpr.constructor_list_or_record_decl_expr

val constructor_list_or_record_decl_expr_of_sexp : 
  Sexplib.Sexp.t ->
  constructor_list_or_record_decl_expr

val sexp_of_constructor_list_or_record_decl_expr : 
  constructor_list_or_record_decl_expr ->
  Sexplib.Sexp.t

type inductive_expr = Vernacexpr.inductive_expr

val inductive_expr_of_sexp : Sexplib.Sexp.t -> inductive_expr

val sexp_of_inductive_expr : inductive_expr -> Sexplib.Sexp.t

type one_inductive_expr = Vernacexpr.one_inductive_expr

val one_inductive_expr_of_sexp : Sexplib.Sexp.t -> one_inductive_expr

val sexp_of_one_inductive_expr : one_inductive_expr -> Sexplib.Sexp.t

type proof_expr = Vernacexpr.proof_expr

val proof_expr_of_sexp : Sexplib.Sexp.t -> proof_expr

val sexp_of_proof_expr : proof_expr -> Sexplib.Sexp.t

type proof_end = Vernacexpr.proof_end

val proof_end_of_sexp : Sexplib.Sexp.t -> proof_end

val sexp_of_proof_end : proof_end -> Sexplib.Sexp.t

type scheme = Vernacexpr.scheme

val scheme_of_sexp : Sexplib.Sexp.t -> scheme

val sexp_of_scheme : scheme -> Sexplib.Sexp.t

type section_subset_expr = Vernacexpr.section_subset_expr

val section_subset_expr_of_sexp : Sexplib.Sexp.t -> section_subset_expr

val sexp_of_section_subset_expr : section_subset_expr -> Sexplib.Sexp.t

type extend_name = Vernacexpr.extend_name

val extend_name_of_sexp : Sexplib.Sexp.t -> extend_name

val sexp_of_extend_name : extend_name -> Sexplib.Sexp.t

type register_kind = Vernacexpr.register_kind

val register_kind_of_sexp : Sexplib.Sexp.t -> register_kind

val sexp_of_register_kind : register_kind -> Sexplib.Sexp.t

type module_ast_inl = Vernacexpr.module_ast_inl

val module_ast_inl_of_sexp : Sexplib.Sexp.t -> module_ast_inl

val sexp_of_module_ast_inl : module_ast_inl -> Sexplib.Sexp.t

type module_binder = Vernacexpr.module_binder

val module_binder_of_sexp : Sexplib.Sexp.t -> module_binder

val sexp_of_module_binder : module_binder -> Sexplib.Sexp.t

type vernac_expr = Vernacexpr.vernac_expr

val vernac_expr_of_sexp : Sexplib.Sexp.t -> vernac_expr

val sexp_of_vernac_expr : vernac_expr -> Sexplib.Sexp.t

val vernac_expr_of_yojson : 
  Yojson.Safe.t ->
  (vernac_expr, string) Result.result

val vernac_expr_to_yojson : vernac_expr -> Yojson.Safe.t

type vernac_control = Vernacexpr.vernac_control

val vernac_control_of_sexp : Sexplib.Sexp.t -> vernac_control

val sexp_of_vernac_control : vernac_control -> Sexplib.Sexp.t

val vernac_control_of_yojson : 
  Yojson.Safe.t ->
  (vernac_control, string) Result.result

val vernac_control_to_yojson : vernac_control -> Yojson.Safe.t

package coq-serapi