package coq-serapi

  1. Overview
  2. Docs
package coq-serapi
Legend:
Library
Module
Module type
Parameter
Class
Class type
type infix_flag = bool
val sexp_of_infix_flag : infix_flag -> Sexplib0.Sexp.t
val infix_flag_of_sexp : Sexplib0.Sexp.t -> infix_flag
val infix_flag_to_yojson : infix_flag -> Yojson.Safe.t
val infix_flag_of_yojson : Yojson.Safe.t -> infix_flag Ppx_deriving_yojson_runtime.error_or
type scope_name = string
val sexp_of_scope_name : scope_name -> Sexplib0.Sexp.t
val scope_name_of_sexp : Sexplib0.Sexp.t -> scope_name
val scope_name_to_yojson : scope_name -> Yojson.Safe.t
val scope_name_of_yojson : Yojson.Safe.t -> scope_name Ppx_deriving_yojson_runtime.error_or
type notation_format = Vernacexpr.notation_format =
  1. | TextFormat of Names.lstring
val sexp_of_notation_format : notation_format -> Sexplib0.Sexp.t
val notation_format_of_sexp : Sexplib0.Sexp.t -> notation_format
val notation_format_to_yojson : notation_format -> Yojson.Safe.t
val notation_format_of_yojson : Yojson.Safe.t -> notation_format Ppx_deriving_yojson_runtime.error_or
type 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
val sexp_of_syntax_modifier : syntax_modifier -> Sexplib0.Sexp.t
val syntax_modifier_of_sexp : Sexplib0.Sexp.t -> syntax_modifier
val syntax_modifier_to_yojson : syntax_modifier -> Yojson.Safe.t
val syntax_modifier_of_yojson : Yojson.Safe.t -> syntax_modifier Ppx_deriving_yojson_runtime.error_or
type coercion_class = Vernacexpr.coercion_class
val coercion_class_of_sexp : Sexplib.Sexp.t -> coercion_class
val sexp_of_coercion_class : coercion_class -> 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 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 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 sexp_of_fixpoint_expr : fixpoint_expr -> Sexplib0.Sexp.t
val fixpoint_expr_of_sexp : Sexplib0.Sexp.t -> fixpoint_expr
val hash_fold_fixpoint_expr : Ppx_hash_lib.Std.Hash.state -> fixpoint_expr -> Ppx_hash_lib.Std.Hash.state
val hash_fixpoint_expr : fixpoint_expr -> Ppx_hash_lib.Std.Hash.hash_value
val compare_fixpoint_expr : fixpoint_expr -> fixpoint_expr -> int
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 notation_declaration = Vernacexpr.notation_declaration
val notation_declaration_of_sexp : Sexplib.Sexp.t -> notation_declaration
val sexp_of_notation_declaration : notation_declaration -> 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 discharge = Vernacexpr.discharge =
  1. | DoDischarge
  2. | NoDischarge
val sexp_of_discharge : discharge -> Sexplib0.Sexp.t
val discharge_of_sexp : Sexplib0.Sexp.t -> discharge
val discharge_to_yojson : discharge -> Yojson.Safe.t
val discharge_of_yojson : Yojson.Safe.t -> discharge Ppx_deriving_yojson_runtime.error_or
type equality_scheme_type = Vernacexpr.equality_scheme_type =
  1. | SchemeBooleanEquality
  2. | SchemeEquality
val sexp_of_equality_scheme_type : equality_scheme_type -> Sexplib0.Sexp.t
val equality_scheme_type_of_sexp : Sexplib0.Sexp.t -> equality_scheme_type
val equality_scheme_type_to_yojson : equality_scheme_type -> Yojson.Safe.t
val equality_scheme_type_of_yojson : Yojson.Safe.t -> equality_scheme_type Ppx_deriving_yojson_runtime.error_or
type import_categories = Vernacexpr.import_categories = {
  1. negative : bool;
  2. import_cats : string CAst.t list;
}
val sexp_of_import_categories : import_categories -> Sexplib0.Sexp.t
val import_categories_of_sexp : Sexplib0.Sexp.t -> import_categories
val import_categories_to_yojson : import_categories -> Yojson.Safe.t
val import_categories_of_yojson : Yojson.Safe.t -> import_categories Ppx_deriving_yojson_runtime.error_or
type export_with_cats = export_flag * import_categories option
val sexp_of_export_with_cats : export_with_cats -> Sexplib0.Sexp.t
val export_with_cats_of_sexp : Sexplib0.Sexp.t -> export_with_cats
val export_with_cats_to_yojson : export_with_cats -> Yojson.Safe.t
val export_with_cats_of_yojson : Yojson.Safe.t -> export_with_cats Ppx_deriving_yojson_runtime.error_or
type one_import_filter_name = Libnames.qualid * bool
val sexp_of_one_import_filter_name : one_import_filter_name -> Sexplib0.Sexp.t
val one_import_filter_name_of_sexp : Sexplib0.Sexp.t -> one_import_filter_name
val one_import_filter_name_to_yojson : one_import_filter_name -> Yojson.Safe.t
val one_import_filter_name_of_yojson : Yojson.Safe.t -> one_import_filter_name Ppx_deriving_yojson_runtime.error_or
type import_filter_expr = Vernacexpr.import_filter_expr =
  1. | ImportAll
  2. | ImportNames of one_import_filter_name list
val sexp_of_import_filter_expr : import_filter_expr -> Sexplib0.Sexp.t
val import_filter_expr_of_sexp : Sexplib0.Sexp.t -> import_filter_expr
val import_filter_expr_to_yojson : import_filter_expr -> Yojson.Safe.t
val import_filter_expr_of_yojson : Yojson.Safe.t -> import_filter_expr Ppx_deriving_yojson_runtime.error_or
type hint_info_expr = Constrexpr.constr_pattern_expr Typeclasses.hint_info_gen
val sexp_of_hint_info_expr : hint_info_expr -> Sexplib0.Sexp.t
val hint_info_expr_of_sexp : Sexplib0.Sexp.t -> hint_info_expr
val hint_info_expr_to_yojson : hint_info_expr -> Yojson.Safe.t
val hint_info_expr_of_yojson : Yojson.Safe.t -> hint_info_expr Ppx_deriving_yojson_runtime.error_or
type reference_or_constr = Vernacexpr.reference_or_constr =
  1. | HintsReference of Libnames.qualid
  2. | HintsConstr of Constrexpr.constr_expr
val sexp_of_reference_or_constr : reference_or_constr -> Sexplib0.Sexp.t
val reference_or_constr_of_sexp : Sexplib0.Sexp.t -> reference_or_constr
val reference_or_constr_to_yojson : reference_or_constr -> Yojson.Safe.t
val reference_or_constr_of_yojson : Yojson.Safe.t -> reference_or_constr Ppx_deriving_yojson_runtime.error_or
type 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
val sexp_of_hints_expr : hints_expr -> Sexplib0.Sexp.t
val hints_expr_of_sexp : Sexplib0.Sexp.t -> hints_expr
val hints_expr_to_yojson : hints_expr -> Yojson.Safe.t
val hints_expr_of_yojson : Yojson.Safe.t -> hints_expr Ppx_deriving_yojson_runtime.error_or
type 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;
}
val sexp_of_vernac_one_argument_status : vernac_one_argument_status -> Sexplib0.Sexp.t
val vernac_one_argument_status_of_sexp : Sexplib0.Sexp.t -> vernac_one_argument_status
val vernac_one_argument_status_to_yojson : vernac_one_argument_status -> Yojson.Safe.t
val vernac_one_argument_status_of_yojson : Yojson.Safe.t -> vernac_one_argument_status Ppx_deriving_yojson_runtime.error_or
type vernac_argument_status = Vernacexpr.vernac_argument_status =
  1. | VolatileArg
  2. | BidiArg
  3. | RealArg of vernac_one_argument_status
val sexp_of_vernac_argument_status : vernac_argument_status -> Sexplib0.Sexp.t
val vernac_argument_status_of_sexp : Sexplib0.Sexp.t -> vernac_argument_status
val vernac_argument_status_to_yojson : vernac_argument_status -> Yojson.Safe.t
val vernac_argument_status_of_yojson : Yojson.Safe.t -> vernac_argument_status Ppx_deriving_yojson_runtime.error_or
type arguments_modifier = [
  1. | `DefaultImplicits
  2. | `ClearScopes
  3. | `ReductionNeverUnfold
  4. | `ExtraScopes
  5. | `ClearImplicits
  6. | `ClearBidiHint
  7. | `Assert
  8. | `Rename
  9. | `ReductionDontExposeCase
]
val sexp_of_arguments_modifier : arguments_modifier -> Sexplib0.Sexp.t
val arguments_modifier_of_sexp : Sexplib0.Sexp.t -> arguments_modifier
val __arguments_modifier_of_sexp__ : Sexplib0.Sexp.t -> arguments_modifier
val arguments_modifier_to_yojson : arguments_modifier -> Yojson.Safe.t
val arguments_modifier_of_yojson : Yojson.Safe.t -> arguments_modifier Ppx_deriving_yojson_runtime.error_or
type option_setting = Vernacexpr.option_setting =
  1. | OptionUnset
  2. | OptionSetTrue
  3. | OptionSetInt of int
  4. | OptionSetString of string
val sexp_of_option_setting : option_setting -> Sexplib0.Sexp.t
val option_setting_of_sexp : Sexplib0.Sexp.t -> option_setting
val option_setting_to_yojson : option_setting -> Yojson.Safe.t
val option_setting_of_yojson : Yojson.Safe.t -> option_setting Ppx_deriving_yojson_runtime.error_or
type notation_enable_modifier = Vernacexpr.notation_enable_modifier =
  1. | EnableNotationEntry of Constrexpr.notation_entry CAst.t
  2. | EnableNotationOnly of Notationextern.notation_use
  3. | EnableNotationAll
val sexp_of_notation_enable_modifier : notation_enable_modifier -> Sexplib0.Sexp.t
val notation_enable_modifier_of_sexp : Sexplib0.Sexp.t -> notation_enable_modifier
val notation_enable_modifier_to_yojson : notation_enable_modifier -> Yojson.Safe.t
val notation_enable_modifier_of_yojson : Yojson.Safe.t -> notation_enable_modifier Ppx_deriving_yojson_runtime.error_or
type 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
val sexp_of_synterp_vernac_expr : synterp_vernac_expr -> Sexplib0.Sexp.t
val synterp_vernac_expr_of_sexp : Sexplib0.Sexp.t -> synterp_vernac_expr
val synterp_vernac_expr_to_yojson : synterp_vernac_expr -> Yojson.Safe.t
val synterp_vernac_expr_of_yojson : Yojson.Safe.t -> synterp_vernac_expr Ppx_deriving_yojson_runtime.error_or
type 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
val sexp_of_synpure_vernac_expr : synpure_vernac_expr -> Sexplib0.Sexp.t
val synpure_vernac_expr_of_sexp : Sexplib0.Sexp.t -> synpure_vernac_expr
val synpure_vernac_expr_to_yojson : synpure_vernac_expr -> Yojson.Safe.t
val synpure_vernac_expr_of_yojson : Yojson.Safe.t -> synpure_vernac_expr Ppx_deriving_yojson_runtime.error_or
type 'a vernac_expr_gen = 'a Vernacexpr.vernac_expr_gen =
  1. | VernacSynterp of 'a
  2. | VernacSynPure of synpure_vernac_expr
val sexp_of_vernac_expr_gen : ('a -> Sexplib0.Sexp.t) -> 'a vernac_expr_gen -> Sexplib0.Sexp.t
val vernac_expr_gen_of_sexp : (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a vernac_expr_gen
val vernac_expr_gen_to_yojson : ('a -> Yojson.Safe.t) -> 'a vernac_expr_gen -> Yojson.Safe.t
val vernac_expr_gen_of_yojson : (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) -> Yojson.Safe.t -> 'a vernac_expr_gen Ppx_deriving_yojson_runtime.error_or
type control_flag = Vernacexpr.control_flag =
  1. | ControlTime
  2. | ControlRedirect of string
  3. | ControlTimeout of int
  4. | ControlFail
  5. | ControlSucceed
val sexp_of_control_flag : control_flag -> Sexplib0.Sexp.t
val control_flag_of_sexp : Sexplib0.Sexp.t -> control_flag
val control_flag_to_yojson : control_flag -> Yojson.Safe.t
val control_flag_of_yojson : Yojson.Safe.t -> control_flag Ppx_deriving_yojson_runtime.error_or
type ('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;
}
val sexp_of_vernac_control_gen_r : ('a -> Sexplib0.Sexp.t) -> ('b -> Sexplib0.Sexp.t) -> ('a, 'b) vernac_control_gen_r -> Sexplib0.Sexp.t
val vernac_control_gen_r_of_sexp : (Sexplib0.Sexp.t -> 'a) -> (Sexplib0.Sexp.t -> 'b) -> Sexplib0.Sexp.t -> ('a, 'b) vernac_control_gen_r
val vernac_control_gen_r_to_yojson : ('a -> Yojson.Safe.t) -> ('b -> Yojson.Safe.t) -> ('a, 'b) vernac_control_gen_r -> Yojson.Safe.t
val vernac_control_gen_r_of_yojson : (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) -> (Yojson.Safe.t -> 'b Ppx_deriving_yojson_runtime.error_or) -> Yojson.Safe.t -> ('a, 'b) vernac_control_gen_r Ppx_deriving_yojson_runtime.error_or
type 'a vernac_control_gen = (control_flag, 'a) vernac_control_gen_r CAst.t
val sexp_of_vernac_control_gen : ('a -> Sexplib0.Sexp.t) -> 'a vernac_control_gen -> Sexplib0.Sexp.t
val vernac_control_gen_of_sexp : (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a vernac_control_gen
val vernac_control_gen_to_yojson : ('a -> Yojson.Safe.t) -> 'a vernac_control_gen -> Yojson.Safe.t
val vernac_control_gen_of_yojson : (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) -> Yojson.Safe.t -> 'a vernac_control_gen Ppx_deriving_yojson_runtime.error_or
val sexp_of_vernac_control : vernac_control -> Sexplib0.Sexp.t
val vernac_control_of_sexp : Sexplib0.Sexp.t -> vernac_control
val vernac_control_to_yojson : vernac_control -> Yojson.Safe.t
val vernac_control_of_yojson : Yojson.Safe.t -> vernac_control Ppx_deriving_yojson_runtime.error_or
val hash_fold_vernac_control : Ppx_hash_lib.Std.Hash.state -> vernac_control -> Ppx_hash_lib.Std.Hash.state
val hash_vernac_control : vernac_control -> Ppx_hash_lib.Std.Hash.hash_value
val 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