package coq-serapi

  1. Overview
  2. Docs
Serialization library and protocol for machine interaction with the Coq proof assistant

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (38)

Authors

  1. E
    Emilio Jesús Gallego Arias
  2. K
    Karl Palmskog
  3. C
    Clément Pit-Claudel
  4. K
    Kaiyu Yang

Maintainers

  1. E
    e@x80.org

Sources

coq-serapi-8.16.0.0.16.1.tbz
sha256=f1070e6fa36ecf042319a14f621f26a331075f3777dfb85a0afbac6e3323e9d4
sha512=efbd947aa6750672f089b7b8604c798033793510eea1c45f4265df5f548b2ecdd3e69d5cb49b0714c09de1012fe358f618c9b1f4610a33339a151b4fdac42321

doc/coq-serapi.serlib/Serlib/Ser_vernacexpr/index.html

Module Serlib.Ser_vernacexprSource

Sourcetype infix_flag = bool
Sourceval sexp_of_infix_flag : infix_flag -> Sexplib0.Sexp.t
Sourceval infix_flag_of_sexp : Sexplib0.Sexp.t -> infix_flag
Sourceval infix_flag_to_yojson : infix_flag -> Yojson.Safe.t
Sourcetype scope_name = string
Sourceval sexp_of_scope_name : scope_name -> Sexplib0.Sexp.t
Sourceval scope_name_of_sexp : Sexplib0.Sexp.t -> scope_name
Sourceval scope_name_to_yojson : scope_name -> Yojson.Safe.t
Sourcetype notation_format = Vernacexpr.notation_format =
  1. | TextFormat of Names.lstring
  2. | ExtraFormat of string * Names.lstring
Sourceval sexp_of_notation_format : notation_format -> Sexplib0.Sexp.t
Sourceval notation_format_of_sexp : Sexplib0.Sexp.t -> notation_format
Sourceval notation_format_to_yojson : notation_format -> Yojson.Safe.t
Sourcetype syntax_modifier = Vernacexpr.syntax_modifier =
  1. | SetItemLevel of string list * Notation_term.constr_as_binder_kind option * Extend.production_level
  2. | SetItemScope of string list * scope_name
  3. | SetLevel of int
  4. | SetCustomEntry of string * int option
  5. | SetAssoc of Gramlib.Gramext.g_assoc
  6. | SetEntryType of string * Extend.simple_constr_prod_entry_key
  7. | SetOnlyParsing
  8. | SetOnlyPrinting
  9. | SetFormat of notation_format
Sourceval sexp_of_syntax_modifier : syntax_modifier -> Sexplib0.Sexp.t
Sourceval syntax_modifier_of_sexp : Sexplib0.Sexp.t -> syntax_modifier
Sourceval syntax_modifier_to_yojson : syntax_modifier -> Yojson.Safe.t
Sourcetype class_rawexpr = Vernacexpr.class_rawexpr
Sourceval class_rawexpr_of_sexp : Sexplib.Sexp.t -> class_rawexpr
Sourceval sexp_of_class_rawexpr : class_rawexpr -> Sexplib.Sexp.t
Sourcetype goal_reference = Vernacexpr.goal_reference
Sourceval goal_reference_of_sexp : Sexplib.Sexp.t -> goal_reference
Sourceval sexp_of_goal_reference : goal_reference -> Sexplib.Sexp.t
Sourcetype printable = Vernacexpr.printable
Sourceval printable_of_sexp : Sexplib.Sexp.t -> printable
Sourceval sexp_of_printable : printable -> Sexplib.Sexp.t
Sourcetype search_item = Vernacexpr.search_item
Sourceval search_item_of_sexp : Sexplib.Sexp.t -> search_item
Sourceval sexp_of_search_item : search_item -> Sexplib.Sexp.t
Sourcetype searchable = Vernacexpr.searchable
Sourceval searchable_of_sexp : Sexplib.Sexp.t -> searchable
Sourceval sexp_of_searchable : searchable -> Sexplib.Sexp.t
Sourcetype locatable = Vernacexpr.locatable
Sourceval locatable_of_sexp : Sexplib.Sexp.t -> locatable
Sourceval sexp_of_locatable : locatable -> Sexplib.Sexp.t
Sourcetype showable = Vernacexpr.showable
Sourceval showable_of_sexp : Sexplib.Sexp.t -> showable
Sourceval sexp_of_showable : showable -> Sexplib.Sexp.t
Sourcetype comment = Vernacexpr.comment
Sourceval comment_of_sexp : Sexplib.Sexp.t -> comment
Sourceval sexp_of_comment : comment -> Sexplib.Sexp.t
Sourcetype search_restriction = Vernacexpr.search_restriction
Sourceval search_restriction_of_sexp : Sexplib.Sexp.t -> search_restriction
Sourceval sexp_of_search_restriction : search_restriction -> Sexplib.Sexp.t
Sourcetype verbose_flag = Vernacexpr.verbose_flag
Sourceval verbose_flag_of_sexp : Sexplib.Sexp.t -> verbose_flag
Sourceval sexp_of_verbose_flag : verbose_flag -> Sexplib.Sexp.t
Sourcetype coercion_flag = Vernacexpr.coercion_flag
Sourceval coercion_flag_of_sexp : Sexplib.Sexp.t -> coercion_flag
Sourceval sexp_of_coercion_flag : coercion_flag -> Sexplib.Sexp.t
Sourcetype instance_flag = Vernacexpr.instance_flag
Sourceval instance_flag_of_sexp : Sexplib.Sexp.t -> instance_flag
Sourceval sexp_of_instance_flag : instance_flag -> Sexplib.Sexp.t
Sourcetype export_flag = Vernacexpr.export_flag
Sourceval export_flag_of_sexp : Sexplib.Sexp.t -> export_flag
Sourceval sexp_of_export_flag : export_flag -> Sexplib.Sexp.t
Sourcetype locality_flag = Vernacexpr.locality_flag
Sourceval locality_flag_of_sexp : Sexplib.Sexp.t -> locality_flag
Sourceval sexp_of_locality_flag : locality_flag -> Sexplib.Sexp.t
Sourcetype definition_expr = Vernacexpr.definition_expr
Sourceval definition_expr_of_sexp : Sexplib.Sexp.t -> definition_expr
Sourceval sexp_of_definition_expr : definition_expr -> Sexplib.Sexp.t
Sourcetype fixpoint_expr = Vernacexpr.fixpoint_expr
Sourceval sexp_of_fixpoint_expr : fixpoint_expr -> Sexplib0.Sexp.t
Sourceval fixpoint_expr_of_sexp : Sexplib0.Sexp.t -> fixpoint_expr
Sourceval hash_fold_fixpoint_expr : Ppx_hash_lib.Std.Hash.state -> fixpoint_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_fixpoint_expr : fixpoint_expr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_fixpoint_expr : fixpoint_expr -> fixpoint_expr -> int
Sourcetype cofixpoint_expr = Vernacexpr.cofixpoint_expr
Sourceval cofixpoint_expr_of_sexp : Sexplib.Sexp.t -> cofixpoint_expr
Sourceval sexp_of_cofixpoint_expr : cofixpoint_expr -> Sexplib.Sexp.t
Sourcetype local_decl_expr = Vernacexpr.local_decl_expr
Sourceval local_decl_expr_of_sexp : Sexplib.Sexp.t -> local_decl_expr
Sourceval sexp_of_local_decl_expr : local_decl_expr -> Sexplib.Sexp.t
Sourcetype inductive_kind = Vernacexpr.inductive_kind
Sourceval inductive_kind_of_sexp : Sexplib.Sexp.t -> inductive_kind
Sourceval sexp_of_inductive_kind : inductive_kind -> Sexplib.Sexp.t
Sourcetype decl_notation = Vernacexpr.decl_notation
Sourceval decl_notation_of_sexp : Sexplib.Sexp.t -> decl_notation
Sourceval sexp_of_decl_notation : decl_notation -> Sexplib.Sexp.t
Sourcetype simple_binder = Vernacexpr.simple_binder
Sourceval simple_binder_of_sexp : Sexplib.Sexp.t -> simple_binder
Sourceval sexp_of_simple_binder : simple_binder -> Sexplib.Sexp.t
Sourcetype class_binder = Vernacexpr.class_binder
Sourceval class_binder_of_sexp : Sexplib.Sexp.t -> class_binder
Sourceval sexp_of_class_binder : class_binder -> Sexplib.Sexp.t
Sourcetype 'a with_coercion = 'a Vernacexpr.with_coercion
Sourceval with_coercion_of_sexp : (Sexplib.Sexp.t -> 'a) -> Sexplib.Sexp.t -> 'a with_coercion
Sourceval sexp_of_with_coercion : ('a -> Sexplib.Sexp.t) -> 'a with_coercion -> Sexplib.Sexp.t
Sourcetype constructor_expr = Vernacexpr.constructor_expr
Sourceval constructor_expr_of_sexp : Sexplib.Sexp.t -> constructor_expr
Sourceval sexp_of_constructor_expr : constructor_expr -> Sexplib.Sexp.t
Sourcetype constructor_list_or_record_decl_expr = Vernacexpr.constructor_list_or_record_decl_expr
Sourceval constructor_list_or_record_decl_expr_of_sexp : Sexplib.Sexp.t -> constructor_list_or_record_decl_expr
Sourceval sexp_of_constructor_list_or_record_decl_expr : constructor_list_or_record_decl_expr -> Sexplib.Sexp.t
Sourcetype inductive_expr = Vernacexpr.inductive_expr
Sourceval inductive_expr_of_sexp : Sexplib.Sexp.t -> inductive_expr
Sourceval sexp_of_inductive_expr : inductive_expr -> Sexplib.Sexp.t
Sourcetype one_inductive_expr = Vernacexpr.one_inductive_expr
Sourceval one_inductive_expr_of_sexp : Sexplib.Sexp.t -> one_inductive_expr
Sourceval sexp_of_one_inductive_expr : one_inductive_expr -> Sexplib.Sexp.t
Sourcetype proof_expr = Vernacexpr.proof_expr
Sourceval proof_expr_of_sexp : Sexplib.Sexp.t -> proof_expr
Sourceval sexp_of_proof_expr : proof_expr -> Sexplib.Sexp.t
Sourcetype proof_end = Vernacexpr.proof_end
Sourceval proof_end_of_sexp : Sexplib.Sexp.t -> proof_end
Sourceval sexp_of_proof_end : proof_end -> Sexplib.Sexp.t
Sourcetype scheme = Vernacexpr.scheme
Sourceval scheme_of_sexp : Sexplib.Sexp.t -> scheme
Sourceval sexp_of_scheme : scheme -> Sexplib.Sexp.t
Sourcetype section_subset_expr = Vernacexpr.section_subset_expr
Sourceval section_subset_expr_of_sexp : Sexplib.Sexp.t -> section_subset_expr
Sourceval sexp_of_section_subset_expr : section_subset_expr -> Sexplib.Sexp.t
Sourcetype extend_name = Vernacexpr.extend_name
Sourceval extend_name_of_sexp : Sexplib.Sexp.t -> extend_name
Sourceval sexp_of_extend_name : extend_name -> Sexplib.Sexp.t
Sourcetype register_kind = Vernacexpr.register_kind
Sourceval register_kind_of_sexp : Sexplib.Sexp.t -> register_kind
Sourceval sexp_of_register_kind : register_kind -> Sexplib.Sexp.t
Sourcetype module_ast_inl = Vernacexpr.module_ast_inl
Sourceval module_ast_inl_of_sexp : Sexplib.Sexp.t -> module_ast_inl
Sourceval sexp_of_module_ast_inl : module_ast_inl -> Sexplib.Sexp.t
Sourcetype module_binder = Vernacexpr.module_binder
Sourceval module_binder_of_sexp : Sexplib.Sexp.t -> module_binder
Sourceval sexp_of_module_binder : module_binder -> Sexplib.Sexp.t
Sourcetype discharge = Vernacexpr.discharge =
  1. | DoDischarge
  2. | NoDischarge
Sourceval sexp_of_discharge : discharge -> Sexplib0.Sexp.t
Sourceval discharge_of_sexp : Sexplib0.Sexp.t -> discharge
Sourceval discharge_to_yojson : discharge -> Yojson.Safe.t
Sourcetype equality_scheme_type = Vernacexpr.equality_scheme_type =
  1. | SchemeBooleanEquality
  2. | SchemeEquality
Sourceval sexp_of_equality_scheme_type : equality_scheme_type -> Sexplib0.Sexp.t
Sourceval equality_scheme_type_of_sexp : Sexplib0.Sexp.t -> equality_scheme_type
Sourceval equality_scheme_type_to_yojson : equality_scheme_type -> Yojson.Safe.t
Sourcetype import_categories = Vernacexpr.import_categories = {
  1. negative : bool;
  2. import_cats : string CAst.t list;
}
Sourceval sexp_of_import_categories : import_categories -> Sexplib0.Sexp.t
Sourceval import_categories_of_sexp : Sexplib0.Sexp.t -> import_categories
Sourceval import_categories_to_yojson : import_categories -> Yojson.Safe.t
Sourcetype export_with_cats = export_flag * import_categories option
Sourceval sexp_of_export_with_cats : export_with_cats -> Sexplib0.Sexp.t
Sourceval export_with_cats_of_sexp : Sexplib0.Sexp.t -> export_with_cats
Sourceval export_with_cats_to_yojson : export_with_cats -> Yojson.Safe.t
Sourcetype one_import_filter_name = Libnames.qualid * bool
Sourceval sexp_of_one_import_filter_name : one_import_filter_name -> Sexplib0.Sexp.t
Sourceval one_import_filter_name_of_sexp : Sexplib0.Sexp.t -> one_import_filter_name
Sourceval one_import_filter_name_to_yojson : one_import_filter_name -> Yojson.Safe.t
Sourcetype import_filter_expr = Vernacexpr.import_filter_expr =
  1. | ImportAll
  2. | ImportNames of one_import_filter_name list
Sourceval sexp_of_import_filter_expr : import_filter_expr -> Sexplib0.Sexp.t
Sourceval import_filter_expr_of_sexp : Sexplib0.Sexp.t -> import_filter_expr
Sourceval import_filter_expr_to_yojson : import_filter_expr -> Yojson.Safe.t
Sourcetype hint_info_expr = Constrexpr.constr_pattern_expr Typeclasses.hint_info_gen
Sourceval sexp_of_hint_info_expr : hint_info_expr -> Sexplib0.Sexp.t
Sourceval hint_info_expr_of_sexp : Sexplib0.Sexp.t -> hint_info_expr
Sourceval hint_info_expr_to_yojson : hint_info_expr -> Yojson.Safe.t
Sourcetype reference_or_constr = Vernacexpr.reference_or_constr =
  1. | HintsReference of Libnames.qualid
  2. | HintsConstr of Constrexpr.constr_expr
Sourceval sexp_of_reference_or_constr : reference_or_constr -> Sexplib0.Sexp.t
Sourceval reference_or_constr_of_sexp : Sexplib0.Sexp.t -> reference_or_constr
Sourceval reference_or_constr_to_yojson : reference_or_constr -> Yojson.Safe.t
Sourcetype hints_expr = Vernacexpr.hints_expr =
  1. | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
  2. | HintsResolveIFF of bool * Libnames.qualid list * int option
  3. | HintsImmediate of reference_or_constr list
  4. | HintsUnfold of Libnames.qualid list
  5. | HintsTransparency of Libnames.qualid Hints.hints_transparency_target * bool
  6. | HintsMode of Libnames.qualid * Hints.hint_mode list
  7. | HintsConstructors of Libnames.qualid list
  8. | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
Sourceval sexp_of_hints_expr : hints_expr -> Sexplib0.Sexp.t
Sourceval hints_expr_of_sexp : Sexplib0.Sexp.t -> hints_expr
Sourceval hints_expr_to_yojson : hints_expr -> Yojson.Safe.t
Sourcetype vernac_one_argument_status = Vernacexpr.vernac_one_argument_status = {
  1. name : Names.Name.t;
  2. recarg_like : bool;
  3. notation_scope : string CAst.t option;
  4. implicit_status : Glob_term.binding_kind;
}
Sourceval sexp_of_vernac_one_argument_status : vernac_one_argument_status -> Sexplib0.Sexp.t
Sourceval vernac_one_argument_status_of_sexp : Sexplib0.Sexp.t -> vernac_one_argument_status
Sourceval vernac_one_argument_status_to_yojson : vernac_one_argument_status -> Yojson.Safe.t
Sourcetype vernac_argument_status = Vernacexpr.vernac_argument_status =
  1. | VolatileArg
  2. | BidiArg
  3. | RealArg of vernac_one_argument_status
Sourceval sexp_of_vernac_argument_status : vernac_argument_status -> Sexplib0.Sexp.t
Sourceval vernac_argument_status_of_sexp : Sexplib0.Sexp.t -> vernac_argument_status
Sourceval vernac_argument_status_to_yojson : vernac_argument_status -> Yojson.Safe.t
Sourcetype arguments_modifier = [
  1. | `DefaultImplicits
  2. | `ClearScopes
  3. | `ReductionNeverUnfold
  4. | `ExtraScopes
  5. | `ClearImplicits
  6. | `ClearBidiHint
  7. | `Assert
  8. | `Rename
  9. | `ReductionDontExposeCase
]
Sourceval sexp_of_arguments_modifier : arguments_modifier -> Sexplib0.Sexp.t
Sourceval arguments_modifier_of_sexp : Sexplib0.Sexp.t -> arguments_modifier
Sourceval __arguments_modifier_of_sexp__ : Sexplib0.Sexp.t -> arguments_modifier
Sourceval arguments_modifier_to_yojson : arguments_modifier -> Yojson.Safe.t
Sourcetype option_setting = Vernacexpr.option_setting =
  1. | OptionUnset
  2. | OptionSetTrue
  3. | OptionSetInt of int
  4. | OptionSetString of string
Sourceval sexp_of_option_setting : option_setting -> Sexplib0.Sexp.t
Sourceval option_setting_of_sexp : Sexplib0.Sexp.t -> option_setting
Sourceval option_setting_to_yojson : option_setting -> Yojson.Safe.t
Sourcetype vernac_expr = Vernacexpr.vernac_expr =
  1. | VernacLoad of verbose_flag * string
  2. | VernacReservedNotation of infix_flag * Names.lstring * syntax_modifier CAst.t list
  3. | VernacOpenCloseScope of bool * scope_name
  4. | VernacDeclareScope of scope_name
  5. | VernacDelimiters of scope_name * string option
  6. | VernacBindScope of scope_name * class_rawexpr list
  7. | VernacNotation of infix_flag * Constrexpr.constr_expr * Names.lstring * syntax_modifier CAst.t list * scope_name option
  8. | VernacNotationAddFormat of string * string * string
  9. | VernacDeclareCustomEntry of string
  10. | VernacDefinition of discharge * Decls.definition_object_kind * Constrexpr.name_decl * definition_expr
  11. | VernacStartTheoremProof of Decls.theorem_kind * proof_expr list
  12. | VernacEndProof of proof_end
  13. | VernacExactProof of Constrexpr.constr_expr
  14. | VernacAssumption of discharge * Decls.assumption_object_kind * Declaremods.inline * (Constrexpr.ident_decl list * Constrexpr.constr_expr) with_coercion list
  15. | VernacInductive of inductive_kind * (inductive_expr * decl_notation list) list
  16. | VernacFixpoint of discharge * fixpoint_expr list
  17. | VernacCoFixpoint of discharge * cofixpoint_expr list
  18. | VernacScheme of (Names.lident option * scheme) list
  19. | VernacSchemeEquality of equality_scheme_type * Libnames.qualid Constrexpr.or_by_notation
  20. | VernacCombinedScheme of Names.lident * Names.lident list
  21. | VernacUniverse of Names.lident list
  22. | VernacConstraint of Constrexpr.univ_constraint_expr list
  23. | VernacBeginSection of Names.lident
  24. | VernacEndSegment of Names.lident
  25. | VernacExtraDependency of Libnames.qualid * string * Names.Id.t option
  26. | VernacRequire of Libnames.qualid option * export_with_cats option * (Libnames.qualid * import_filter_expr) list
  27. | VernacImport of export_with_cats * (Libnames.qualid * import_filter_expr) list
  28. | VernacCanonical of Libnames.qualid Constrexpr.or_by_notation
  29. | VernacCoercion of Libnames.qualid Constrexpr.or_by_notation * (class_rawexpr * class_rawexpr) option
  30. | VernacIdentityCoercion of Names.lident * class_rawexpr * class_rawexpr
  31. | VernacNameSectionHypSet of Names.lident * section_subset_expr
  32. | VernacInstance of Constrexpr.name_decl * Constrexpr.local_binder_expr list * Constrexpr.constr_expr * (bool * Constrexpr.constr_expr) option * hint_info_expr
  33. | VernacDeclareInstance of Constrexpr.ident_decl * Constrexpr.local_binder_expr list * Constrexpr.constr_expr * hint_info_expr
  34. | VernacContext of Constrexpr.local_binder_expr list
  35. | VernacExistingInstance of (Libnames.qualid * hint_info_expr) list
  36. | VernacExistingClass of Libnames.qualid
  37. | VernacDeclareModule of export_with_cats option * Names.lident * module_binder list * module_ast_inl
  38. | VernacDefineModule of export_with_cats option * Names.lident * module_binder list * module_ast_inl Declaremods.module_signature * module_ast_inl list
  39. | VernacDeclareModuleType of Names.lident * module_binder list * module_ast_inl list * module_ast_inl list
  40. | VernacInclude of module_ast_inl list
  41. | VernacAddLoadPath of {
    1. implicit : bool;
    2. physical_path : CUnix.physical_path;
    3. logical_path : Names.DirPath.t;
    }
  42. | VernacRemoveLoadPath of string
  43. | VernacAddMLPath of string
  44. | VernacDeclareMLModule of string list
  45. | VernacChdir of string option
  46. | VernacResetName of Names.lident
  47. | VernacResetInitial
  48. | VernacBack of int
  49. | VernacCreateHintDb of string * bool
  50. | VernacRemoveHints of string list * Libnames.qualid list
  51. | VernacHints of string list * hints_expr
  52. | VernacSyntacticDefinition of Names.lident * Names.Id.t list * Constrexpr.constr_expr * syntax_modifier CAst.t list
  53. | VernacArguments of Libnames.qualid Constrexpr.or_by_notation * vernac_argument_status list * (Names.Name.t * Glob_term.binding_kind) list list * arguments_modifier list
  54. | VernacReserve of simple_binder list
  55. | VernacGeneralizable of Names.lident list option
  56. | VernacSetOpacity of Conv_oracle.level * Libnames.qualid Constrexpr.or_by_notation list
  57. | VernacSetStrategy of (Conv_oracle.level * Libnames.qualid Constrexpr.or_by_notation list) list
  58. | VernacSetOption of bool * Goptions.option_name * option_setting
  59. | VernacAddOption of Goptions.option_name * Goptions.table_value list
  60. | VernacRemoveOption of Goptions.option_name * Goptions.table_value list
  61. | VernacMemOption of Goptions.option_name * Goptions.table_value list
  62. | VernacPrintOption of Goptions.option_name
  63. | VernacCheckMayEval of Genredexpr.raw_red_expr option * Goal_select.t option * Constrexpr.constr_expr
  64. | VernacGlobalCheck of Constrexpr.constr_expr
  65. | VernacDeclareReduction of string * Genredexpr.raw_red_expr
  66. | VernacPrint of printable
  67. | VernacSearch of searchable * Goal_select.t option * search_restriction
  68. | VernacLocate of locatable
  69. | VernacRegister of Libnames.qualid * register_kind
  70. | VernacPrimitive of Constrexpr.ident_decl * CPrimitives.op_or_type * Constrexpr.constr_expr option
  71. | VernacComments of comment list
  72. | VernacAbort
  73. | VernacAbortAll
  74. | VernacRestart
  75. | VernacUndo of int
  76. | VernacUndoTo of int
  77. | VernacFocus of int option
  78. | VernacUnfocus
  79. | VernacUnfocused
  80. | VernacBullet of Proof_bullet.t
  81. | VernacSubproof of Goal_select.t option
  82. | VernacEndSubproof
  83. | VernacShow of showable
  84. | VernacCheckGuard
  85. | VernacProof of Genarg.raw_generic_argument option * section_subset_expr option
  86. | VernacProofMode of string
  87. | VernacExtend of extend_name * Genarg.raw_generic_argument list
Sourceval sexp_of_vernac_expr : vernac_expr -> Sexplib0.Sexp.t
Sourceval vernac_expr_of_sexp : Sexplib0.Sexp.t -> vernac_expr
Sourceval vernac_expr_to_yojson : vernac_expr -> Yojson.Safe.t
Sourcetype control_flag = Vernacexpr.control_flag =
  1. | ControlTime of bool
  2. | ControlRedirect of string
  3. | ControlTimeout of int
  4. | ControlFail
  5. | ControlSucceed
Sourceval sexp_of_control_flag : control_flag -> Sexplib0.Sexp.t
Sourceval control_flag_of_sexp : Sexplib0.Sexp.t -> control_flag
Sourceval control_flag_to_yojson : control_flag -> Yojson.Safe.t
Sourcetype vernac_control_r = Vernacexpr.vernac_control_r = {
  1. control : control_flag list;
  2. attrs : Attributes.vernac_flags;
  3. expr : vernac_expr;
}
Sourceval sexp_of_vernac_control_r : vernac_control_r -> Sexplib0.Sexp.t
Sourceval vernac_control_r_of_sexp : Sexplib0.Sexp.t -> vernac_control_r
Sourceval vernac_control_r_to_yojson : vernac_control_r -> Yojson.Safe.t
Sourcetype vernac_control = vernac_control_r CAst.t
Sourceval sexp_of_vernac_control : vernac_control -> Sexplib0.Sexp.t
Sourceval vernac_control_of_sexp : Sexplib0.Sexp.t -> vernac_control
Sourceval vernac_control_to_yojson : vernac_control -> Yojson.Safe.t
Sourceval hash_fold_vernac_control : Ppx_hash_lib.Std.Hash.state -> vernac_control -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_vernac_control : vernac_control -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_vernac_control : vernac_control -> vernac_control -> int
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct