package coq-serapi

  1. Overview
  2. Docs
package coq-serapi
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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
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.notation_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 coercion_class = Vernacexpr.coercion_class
Sourceval coercion_class_of_sexp : Sexplib.Sexp.t -> coercion_class
Sourceval sexp_of_coercion_class : coercion_class -> 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 notation_declaration = Vernacexpr.notation_declaration
Sourceval notation_declaration_of_sexp : Sexplib.Sexp.t -> notation_declaration
Sourceval sexp_of_notation_declaration : notation_declaration -> 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 list;
  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 notation_enable_modifier = Vernacexpr.notation_enable_modifier =
  1. | EnableNotationEntry of Constrexpr.notation_entry CAst.t
  2. | EnableNotationOnly of Notationextern.notation_use
  3. | EnableNotationAll
Sourceval sexp_of_notation_enable_modifier : notation_enable_modifier -> Sexplib0.Sexp.t
Sourceval notation_enable_modifier_of_sexp : Sexplib0.Sexp.t -> notation_enable_modifier
Sourceval notation_enable_modifier_to_yojson : notation_enable_modifier -> Yojson.Safe.t
Sourcetype synterp_vernac_expr = Vernacexpr.synterp_vernac_expr =
  1. | VernacLoad of verbose_flag * string
  2. | VernacReservedNotation of infix_flag * Names.lstring * syntax_modifier CAst.t list
  3. | VernacNotation of infix_flag * notation_declaration
  4. | VernacDeclareCustomEntry of string
  5. | VernacBeginSection of Names.lident
  6. | VernacEndSegment of Names.lident
  7. | VernacRequire of Libnames.qualid option * export_with_cats option * (Libnames.qualid * import_filter_expr) list
  8. | VernacImport of export_with_cats * (Libnames.qualid * import_filter_expr) list
  9. | VernacDeclareModule of export_with_cats option * Names.lident * module_binder list * module_ast_inl
  10. | VernacDefineModule of export_with_cats option * Names.lident * module_binder list * module_ast_inl Declaremods.module_signature * module_ast_inl list
  11. | VernacDeclareModuleType of Names.lident * module_binder list * module_ast_inl list * module_ast_inl list
  12. | VernacInclude of module_ast_inl list
  13. | VernacDeclareMLModule of string list
  14. | VernacChdir of string option
  15. | VernacExtraDependency of Libnames.qualid * string * Names.Id.t option
  16. | VernacSetOption of bool * Goptions.option_name * option_setting
  17. | VernacProofMode of string
  18. | VernacExtend of extend_name * Genarg.raw_generic_argument list
Sourceval sexp_of_synterp_vernac_expr : synterp_vernac_expr -> Sexplib0.Sexp.t
Sourceval synterp_vernac_expr_of_sexp : Sexplib0.Sexp.t -> synterp_vernac_expr
Sourceval synterp_vernac_expr_to_yojson : synterp_vernac_expr -> Yojson.Safe.t
Sourcetype synpure_vernac_expr = Vernacexpr.synpure_vernac_expr =
  1. | VernacOpenCloseScope of bool * scope_name
  2. | VernacDeclareScope of scope_name
  3. | VernacDelimiters of scope_name * string option
  4. | VernacBindScope of scope_name * coercion_class list
  5. | VernacEnableNotation of bool * (string, Names.Id.t list * Libnames.qualid) Util.union option * Constrexpr.constr_expr option * notation_enable_modifier list * Constrexpr.notation_with_optional_scope option
  6. | VernacDefinition of discharge * Decls.definition_object_kind * Constrexpr.name_decl * definition_expr
  7. | VernacStartTheoremProof of Decls.theorem_kind * proof_expr list
  8. | VernacEndProof of proof_end
  9. | VernacExactProof of Constrexpr.constr_expr
  10. | VernacAssumption of discharge * Decls.assumption_object_kind * Declaremods.inline * (Constrexpr.ident_decl list * Constrexpr.constr_expr) with_coercion list
  11. | VernacInductive of inductive_kind * (inductive_expr * notation_declaration list) list
  12. | VernacFixpoint of discharge * fixpoint_expr list
  13. | VernacCoFixpoint of discharge * cofixpoint_expr list
  14. | VernacScheme of (Names.lident option * scheme) list
  15. | VernacSchemeEquality of equality_scheme_type * Libnames.qualid Constrexpr.or_by_notation
  16. | VernacCombinedScheme of Names.lident * Names.lident list
  17. | VernacUniverse of Names.lident list
  18. | VernacConstraint of Constrexpr.univ_constraint_expr list
  19. | VernacCanonical of Libnames.qualid Constrexpr.or_by_notation
  20. | VernacCoercion of Libnames.qualid Constrexpr.or_by_notation * (coercion_class * coercion_class) option
  21. | VernacIdentityCoercion of Names.lident * coercion_class * coercion_class
  22. | VernacNameSectionHypSet of Names.lident * section_subset_expr
  23. | VernacInstance of Constrexpr.name_decl * Constrexpr.local_binder_expr list * Constrexpr.constr_expr * (bool * Constrexpr.constr_expr) option * hint_info_expr
  24. | VernacDeclareInstance of Constrexpr.ident_decl * Constrexpr.local_binder_expr list * Constrexpr.constr_expr * hint_info_expr
  25. | VernacContext of Constrexpr.local_binder_expr list
  26. | VernacExistingInstance of (Libnames.qualid * hint_info_expr) list
  27. | VernacExistingClass of Libnames.qualid
  28. | VernacResetName of Names.lident
  29. | VernacResetInitial
  30. | VernacBack of int
  31. | VernacCreateHintDb of string * bool
  32. | VernacRemoveHints of string list * Libnames.qualid list
  33. | VernacHints of string list * hints_expr
  34. | VernacSyntacticDefinition of Names.lident * Names.Id.t list * Constrexpr.constr_expr * syntax_modifier CAst.t list
  35. | VernacArguments of Libnames.qualid Constrexpr.or_by_notation * vernac_argument_status list * (Names.Name.t * Glob_term.binding_kind) list list * arguments_modifier list
  36. | VernacReserve of simple_binder list
  37. | VernacGeneralizable of Names.lident list option
  38. | VernacSetOpacity of Conv_oracle.level * Libnames.qualid Constrexpr.or_by_notation list
  39. | VernacSetStrategy of (Conv_oracle.level * Libnames.qualid Constrexpr.or_by_notation list) list
  40. | VernacMemOption of Goptions.option_name * Goptions.table_value list
  41. | VernacPrintOption of Goptions.option_name
  42. | VernacCheckMayEval of Genredexpr.raw_red_expr option * Goal_select.t option * Constrexpr.constr_expr
  43. | VernacGlobalCheck of Constrexpr.constr_expr
  44. | VernacDeclareReduction of string * Genredexpr.raw_red_expr
  45. | VernacPrint of printable
  46. | VernacSearch of searchable * Goal_select.t option * search_restriction
  47. | VernacLocate of locatable
  48. | VernacRegister of Libnames.qualid * register_kind
  49. | VernacPrimitive of Constrexpr.ident_decl * CPrimitives.op_or_type * Constrexpr.constr_expr option
  50. | VernacComments of comment list
  51. | VernacAbort
  52. | VernacAbortAll
  53. | VernacRestart
  54. | VernacUndo of int
  55. | VernacUndoTo of int
  56. | VernacFocus of int option
  57. | VernacUnfocus
  58. | VernacUnfocused
  59. | VernacBullet of Proof_bullet.t
  60. | VernacSubproof of Goal_select.t option
  61. | VernacEndSubproof
  62. | VernacShow of showable
  63. | VernacCheckGuard
  64. | VernacValidateProof
  65. | VernacProof of Genarg.raw_generic_argument option * section_subset_expr option
  66. | VernacAddOption of Goptions.option_name * Goptions.table_value list
  67. | VernacRemoveOption of Goptions.option_name * Goptions.table_value list
Sourceval sexp_of_synpure_vernac_expr : synpure_vernac_expr -> Sexplib0.Sexp.t
Sourceval synpure_vernac_expr_of_sexp : Sexplib0.Sexp.t -> synpure_vernac_expr
Sourceval synpure_vernac_expr_to_yojson : synpure_vernac_expr -> Yojson.Safe.t
Sourcetype 'a vernac_expr_gen = 'a Vernacexpr.vernac_expr_gen =
  1. | VernacSynterp of 'a
  2. | VernacSynPure of synpure_vernac_expr
Sourceval sexp_of_vernac_expr_gen : ('a -> Sexplib0.Sexp.t) -> 'a vernac_expr_gen -> Sexplib0.Sexp.t
Sourceval vernac_expr_gen_of_sexp : (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a vernac_expr_gen
Sourceval vernac_expr_gen_to_yojson : ('a -> Yojson.Safe.t) -> 'a vernac_expr_gen -> Yojson.Safe.t
Sourcetype control_flag = Vernacexpr.control_flag =
  1. | ControlTime
  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 ('a, 'b) vernac_control_gen_r = ('a, 'b) Vernacexpr.vernac_control_gen_r = {
  1. control : 'a list;
  2. attrs : Attributes.vernac_flags;
  3. expr : 'b vernac_expr_gen;
}
Sourceval sexp_of_vernac_control_gen_r : ('a -> Sexplib0.Sexp.t) -> ('b -> Sexplib0.Sexp.t) -> ('a, 'b) vernac_control_gen_r -> Sexplib0.Sexp.t
Sourceval vernac_control_gen_r_of_sexp : (Sexplib0.Sexp.t -> 'a) -> (Sexplib0.Sexp.t -> 'b) -> Sexplib0.Sexp.t -> ('a, 'b) vernac_control_gen_r
Sourceval vernac_control_gen_r_to_yojson : ('a -> Yojson.Safe.t) -> ('b -> Yojson.Safe.t) -> ('a, 'b) vernac_control_gen_r -> Yojson.Safe.t
Sourcetype 'a vernac_control_gen = (control_flag, 'a) vernac_control_gen_r CAst.t
Sourceval sexp_of_vernac_control_gen : ('a -> Sexplib0.Sexp.t) -> 'a vernac_control_gen -> Sexplib0.Sexp.t
Sourceval vernac_control_gen_of_sexp : (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a vernac_control_gen
Sourceval vernac_control_gen_to_yojson : ('a -> Yojson.Safe.t) -> 'a vernac_control_gen -> Yojson.Safe.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