package coq-serapi

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type infix_flag = bool
val infix_flag_to_yojson : infix_flag -> Yojson.Safe.t
val sexp_of_infix_flag : infix_flag -> Sexplib0.Sexp.t
val infix_flag_of_sexp : Sexplib0.Sexp.t -> infix_flag
type scope_name = string
val scope_name_to_yojson : scope_name -> Yojson.Safe.t
val sexp_of_scope_name : scope_name -> Sexplib0.Sexp.t
val scope_name_of_sexp : Sexplib0.Sexp.t -> scope_name
type notation_format = Vernacexpr.notation_format =
  1. | TextFormat of Names.lstring
val notation_format_to_yojson : notation_format -> Yojson.Safe.t
val sexp_of_notation_format : notation_format -> Sexplib0.Sexp.t
val notation_format_of_sexp : Sexplib0.Sexp.t -> notation_format
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 syntax_modifier_to_yojson : syntax_modifier -> Yojson.Safe.t
val sexp_of_syntax_modifier : syntax_modifier -> Sexplib0.Sexp.t
val syntax_modifier_of_sexp : Sexplib0.Sexp.t -> syntax_modifier
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 : Base.Hash.state -> fixpoint_expr -> Base.Hash.state
val hash_fixpoint_expr : fixpoint_expr -> Base.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 discharge_to_yojson : discharge -> Yojson.Safe.t
val sexp_of_discharge : discharge -> Sexplib0.Sexp.t
val discharge_of_sexp : Sexplib0.Sexp.t -> discharge
type equality_scheme_type = Vernacexpr.equality_scheme_type =
  1. | SchemeBooleanEquality
  2. | SchemeEquality
val equality_scheme_type_to_yojson : equality_scheme_type -> Yojson.Safe.t
val sexp_of_equality_scheme_type : equality_scheme_type -> Sexplib0.Sexp.t
val equality_scheme_type_of_sexp : Sexplib0.Sexp.t -> equality_scheme_type
type import_categories = Vernacexpr.import_categories = {
  1. negative : bool;
  2. import_cats : string CAst.t list;
}
val import_categories_to_yojson : import_categories -> Yojson.Safe.t
val sexp_of_import_categories : import_categories -> Sexplib0.Sexp.t
val import_categories_of_sexp : Sexplib0.Sexp.t -> import_categories
type export_with_cats = export_flag * import_categories option
val export_with_cats_to_yojson : export_with_cats -> Yojson.Safe.t
val sexp_of_export_with_cats : export_with_cats -> Sexplib0.Sexp.t
val export_with_cats_of_sexp : Sexplib0.Sexp.t -> export_with_cats
type one_import_filter_name = Libnames.qualid * bool
val one_import_filter_name_to_yojson : one_import_filter_name -> Yojson.Safe.t
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
type import_filter_expr = Vernacexpr.import_filter_expr =
  1. | ImportAll
  2. | ImportNames of one_import_filter_name list
val import_filter_expr_to_yojson : import_filter_expr -> Yojson.Safe.t
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 hint_info_expr_to_yojson : hint_info_expr -> Yojson.Safe.t
val sexp_of_hint_info_expr : hint_info_expr -> Sexplib0.Sexp.t
val hint_info_expr_of_sexp : Sexplib0.Sexp.t -> hint_info_expr
type reference_or_constr = Vernacexpr.reference_or_constr =
  1. | HintsReference of Libnames.qualid
  2. | HintsConstr of Constrexpr.constr_expr
val reference_or_constr_to_yojson : reference_or_constr -> Yojson.Safe.t
val sexp_of_reference_or_constr : reference_or_constr -> Sexplib0.Sexp.t
val reference_or_constr_of_sexp : Sexplib0.Sexp.t -> reference_or_constr
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 hints_expr_to_yojson : hints_expr -> Yojson.Safe.t
val sexp_of_hints_expr : hints_expr -> Sexplib0.Sexp.t
val hints_expr_of_sexp : Sexplib0.Sexp.t -> hints_expr
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 vernac_one_argument_status_to_yojson : vernac_one_argument_status -> Yojson.Safe.t
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
type vernac_argument_status = Vernacexpr.vernac_argument_status =
  1. | VolatileArg
  2. | BidiArg
  3. | RealArg of vernac_one_argument_status
val vernac_argument_status_to_yojson : vernac_argument_status -> Yojson.Safe.t
val sexp_of_vernac_argument_status : vernac_argument_status -> Sexplib0.Sexp.t
val vernac_argument_status_of_sexp : Sexplib0.Sexp.t -> vernac_argument_status
type arguments_modifier = [
  1. | `DefaultImplicits
  2. | `ClearScopes
  3. | `ReductionNeverUnfold
  4. | `ExtraScopes
  5. | `ClearImplicits
  6. | `ClearBidiHint
  7. | `Assert
  8. | `Rename
  9. | `ReductionDontExposeCase
]
val arguments_modifier_to_yojson : arguments_modifier -> Yojson.Safe.t
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
type option_setting = Vernacexpr.option_setting =
  1. | OptionUnset
  2. | OptionSetTrue
  3. | OptionSetInt of int
  4. | OptionSetString of string
val option_setting_to_yojson : option_setting -> Yojson.Safe.t
val sexp_of_option_setting : option_setting -> Sexplib0.Sexp.t
val option_setting_of_sexp : Sexplib0.Sexp.t -> option_setting
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 notation_enable_modifier_to_yojson : notation_enable_modifier -> Yojson.Safe.t
val sexp_of_notation_enable_modifier : notation_enable_modifier -> Sexplib0.Sexp.t
val notation_enable_modifier_of_sexp : Sexplib0.Sexp.t -> notation_enable_modifier
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 synterp_vernac_expr_to_yojson : synterp_vernac_expr -> Yojson.Safe.t
val sexp_of_synterp_vernac_expr : synterp_vernac_expr -> Sexplib0.Sexp.t
val synterp_vernac_expr_of_sexp : Sexplib0.Sexp.t -> synterp_vernac_expr
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 synpure_vernac_expr_to_yojson : synpure_vernac_expr -> Yojson.Safe.t
val sexp_of_synpure_vernac_expr : synpure_vernac_expr -> Sexplib0.Sexp.t
val synpure_vernac_expr_of_sexp : Sexplib0.Sexp.t -> synpure_vernac_expr
type 'a vernac_expr_gen = 'a Vernacexpr.vernac_expr_gen =
  1. | VernacSynterp of 'a
  2. | VernacSynPure of synpure_vernac_expr
val vernac_expr_gen_to_yojson : ('a -> Yojson.Safe.t) -> 'a vernac_expr_gen -> Yojson.Safe.t
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
type control_flag = Vernacexpr.control_flag =
  1. | ControlTime
  2. | ControlRedirect of string
  3. | ControlTimeout of int
  4. | ControlFail
  5. | ControlSucceed
val control_flag_to_yojson : control_flag -> Yojson.Safe.t
val sexp_of_control_flag : control_flag -> Sexplib0.Sexp.t
val control_flag_of_sexp : Sexplib0.Sexp.t -> control_flag
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 vernac_control_gen_r_to_yojson : ('a -> Yojson.Safe.t) -> ('b -> Yojson.Safe.t) -> ('a, 'b) vernac_control_gen_r -> Yojson.Safe.t
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
type 'a vernac_control_gen = (control_flag, 'a) vernac_control_gen_r CAst.t
val vernac_control_gen_to_yojson : ('a -> Yojson.Safe.t) -> 'a vernac_control_gen -> Yojson.Safe.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_to_yojson : vernac_control -> Yojson.Safe.t
val sexp_of_vernac_control : vernac_control -> Sexplib0.Sexp.t
val vernac_control_of_sexp : Sexplib0.Sexp.t -> vernac_control
val hash_fold_vernac_control : Base.Hash.state -> vernac_control -> Base.Hash.state
val hash_vernac_control : vernac_control -> Base.Hash.hash_value
val compare_vernac_control : vernac_control -> vernac_control -> int
OCaml

Innovation. Community. Security.