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 hash_fold_infix_flag : Base.Hash.state -> infix_flag -> Base.Hash.state
val hash_infix_flag : infix_flag -> Base.Hash.hash_value
val compare_infix_flag : infix_flag -> infix_flag -> int
type opacity_flag = Vernacexpr.opacity_flag =
  1. | Opaque
  2. | Transparent
val sexp_of_opacity_flag : opacity_flag -> Sexplib0.Sexp.t
val opacity_flag_of_sexp : Sexplib0.Sexp.t -> opacity_flag
val opacity_flag_to_yojson : opacity_flag -> Yojson.Safe.t
val hash_fold_opacity_flag : Base.Hash.state -> opacity_flag -> Base.Hash.state
val hash_opacity_flag : opacity_flag -> Base.Hash.hash_value
val compare_opacity_flag : opacity_flag -> opacity_flag -> int
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 hash_fold_scope_name : Base.Hash.state -> scope_name -> Base.Hash.state
val hash_scope_name : scope_name -> Base.Hash.hash_value
val compare_scope_name : scope_name -> scope_name -> int
type scope_delimiter = Constrexpr.delimiter_depth * scope_name
val sexp_of_scope_delimiter : scope_delimiter -> Sexplib0.Sexp.t
val scope_delimiter_of_sexp : Sexplib0.Sexp.t -> scope_delimiter
val scope_delimiter_to_yojson : scope_delimiter -> Yojson.Safe.t
val hash_fold_scope_delimiter : Base.Hash.state -> scope_delimiter -> Base.Hash.state
val hash_scope_delimiter : scope_delimiter -> Base.Hash.hash_value
val compare_scope_delimiter : scope_delimiter -> scope_delimiter -> int
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 hash_fold_notation_format : Base.Hash.state -> notation_format -> Base.Hash.state
val hash_notation_format : notation_format -> Base.Hash.hash_value
val compare_notation_format : notation_format -> notation_format -> int
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 hash_fold_syntax_modifier : Base.Hash.state -> syntax_modifier -> Base.Hash.state
val hash_syntax_modifier : syntax_modifier -> Base.Hash.hash_value
val compare_syntax_modifier : syntax_modifier -> syntax_modifier -> int
type coercion_class = Vernacexpr.coercion_class =
  1. | FunClass
  2. | SortClass
  3. | RefClass of Libnames.qualid Constrexpr.or_by_notation
val sexp_of_coercion_class : coercion_class -> Sexplib0.Sexp.t
val coercion_class_of_sexp : Sexplib0.Sexp.t -> coercion_class
val coercion_class_to_yojson : coercion_class -> Yojson.Safe.t
val hash_fold_coercion_class : Base.Hash.state -> coercion_class -> Base.Hash.state
val hash_coercion_class : coercion_class -> Base.Hash.hash_value
val compare_coercion_class : coercion_class -> coercion_class -> int
type goal_reference = Vernacexpr.goal_reference =
  1. | OpenSubgoals
  2. | NthGoal of int
  3. | GoalId of Names.Id.t
val sexp_of_goal_reference : goal_reference -> Sexplib0.Sexp.t
val goal_reference_of_sexp : Sexplib0.Sexp.t -> goal_reference
val goal_reference_to_yojson : goal_reference -> Yojson.Safe.t
val hash_fold_goal_reference : Base.Hash.state -> goal_reference -> Base.Hash.state
val hash_goal_reference : goal_reference -> Base.Hash.hash_value
val compare_goal_reference : goal_reference -> goal_reference -> int
type printable = Vernacexpr.printable =
  1. | PrintTypingFlags
  2. | PrintTables
  3. | PrintFullContext
  4. | PrintSectionContext of Libnames.qualid
  5. | PrintInspect of int
  6. | PrintGrammar of string list
  7. | PrintCustomGrammar of string
  8. | PrintKeywords
  9. | PrintLoadPath of Names.DirPath.t option
  10. | PrintLibraries
  11. | PrintModule of Libnames.qualid
  12. | PrintModuleType of Libnames.qualid
  13. | PrintNamespace of Names.DirPath.t
  14. | PrintMLLoadPath
  15. | PrintMLModules
  16. | PrintDebugGC
  17. | PrintName of Libnames.qualid Constrexpr.or_by_notation * UnivNames.full_name_list option
  18. | PrintGraph
  19. | PrintClasses
  20. | PrintTypeclasses
  21. | PrintInstances of Libnames.qualid Constrexpr.or_by_notation
  22. | PrintCoercions
  23. | PrintCoercionPaths of coercion_class * coercion_class
  24. | PrintCanonicalConversions of Libnames.qualid Constrexpr.or_by_notation list
  25. | PrintUniverses of bool * Libnames.qualid list option * string option
  26. | PrintHint of Libnames.qualid Constrexpr.or_by_notation
  27. | PrintHintGoal
  28. | PrintHintDbName of string
  29. | PrintHintDb
  30. | PrintScopes
  31. | PrintScope of string
  32. | PrintVisibility of string option
  33. | PrintAbout of Libnames.qualid Constrexpr.or_by_notation * UnivNames.full_name_list option * Goal_select.t option
  34. | PrintImplicit of Libnames.qualid Constrexpr.or_by_notation
  35. | PrintAssumptions of bool * bool * Libnames.qualid Constrexpr.or_by_notation
  36. | PrintStrategy of Libnames.qualid Constrexpr.or_by_notation option
  37. | PrintRegistered
  38. | PrintRegisteredSchemes
  39. | PrintNotation of Constrexpr.notation_entry * string
val sexp_of_printable : printable -> Sexplib0.Sexp.t
val printable_of_sexp : Sexplib0.Sexp.t -> printable
val printable_to_yojson : printable -> Yojson.Safe.t
val hash_fold_printable : Base.Hash.state -> printable -> Base.Hash.state
val hash_printable : printable -> Base.Hash.hash_value
val compare_printable : printable -> printable -> int
type glob_search_where = Vernacexpr.glob_search_where =
  1. | InHyp
  2. | InConcl
  3. | Anywhere
val sexp_of_glob_search_where : glob_search_where -> Sexplib0.Sexp.t
val glob_search_where_of_sexp : Sexplib0.Sexp.t -> glob_search_where
val glob_search_where_to_yojson : glob_search_where -> Yojson.Safe.t
val hash_fold_glob_search_where : Base.Hash.state -> glob_search_where -> Base.Hash.state
val hash_glob_search_where : glob_search_where -> Base.Hash.hash_value
val compare_glob_search_where : glob_search_where -> glob_search_where -> int
type search_item = Vernacexpr.search_item =
  1. | SearchSubPattern of glob_search_where * bool * Constrexpr.constr_pattern_expr
  2. | SearchString of glob_search_where * bool * string * scope_delimiter option
  3. | SearchKind of Decls.logical_kind
val sexp_of_search_item : search_item -> Sexplib0.Sexp.t
val search_item_of_sexp : Sexplib0.Sexp.t -> search_item
val search_item_to_yojson : search_item -> Yojson.Safe.t
val hash_fold_search_item : Base.Hash.state -> search_item -> Base.Hash.state
val hash_search_item : search_item -> Base.Hash.hash_value
val compare_search_item : search_item -> search_item -> int
type search_request = Vernacexpr.search_request =
  1. | SearchLiteral of search_item
  2. | SearchDisjConj of (bool * search_request) list list
val sexp_of_search_request : search_request -> Sexplib0.Sexp.t
val search_request_of_sexp : Sexplib0.Sexp.t -> search_request
val search_request_to_yojson : search_request -> Yojson.Safe.t
val hash_fold_search_request : Base.Hash.state -> search_request -> Base.Hash.state
val hash_search_request : search_request -> Base.Hash.hash_value
val compare_search_request : search_request -> search_request -> int
type searchable = Vernacexpr.searchable =
  1. | SearchPattern of Constrexpr.constr_pattern_expr
  2. | SearchRewrite of Constrexpr.constr_pattern_expr
  3. | Search of (bool * search_request) list
val sexp_of_searchable : searchable -> Sexplib0.Sexp.t
val searchable_of_sexp : Sexplib0.Sexp.t -> searchable
val searchable_to_yojson : searchable -> Yojson.Safe.t
val hash_fold_searchable : Base.Hash.state -> searchable -> Base.Hash.state
val hash_searchable : searchable -> Base.Hash.hash_value
val compare_searchable : searchable -> searchable -> int
type locatable = Vernacexpr.locatable =
  1. | LocateAny of Libnames.qualid Constrexpr.or_by_notation
  2. | LocateTerm of Libnames.qualid Constrexpr.or_by_notation
  3. | LocateLibrary of Libnames.qualid
  4. | LocateModule of Libnames.qualid
  5. | LocateOther of string * Libnames.qualid
  6. | LocateFile of string
val sexp_of_locatable : locatable -> Sexplib0.Sexp.t
val locatable_of_sexp : Sexplib0.Sexp.t -> locatable
val locatable_to_yojson : locatable -> Yojson.Safe.t
val hash_fold_locatable : Base.Hash.state -> locatable -> Base.Hash.state
val hash_locatable : locatable -> Base.Hash.hash_value
val compare_locatable : locatable -> locatable -> int
type showable = Vernacexpr.showable =
  1. | ShowGoal of goal_reference
  2. | ShowProof
  3. | ShowExistentials
  4. | ShowUniverses
  5. | ShowProofNames
  6. | ShowIntros of bool
  7. | ShowMatch of Libnames.qualid
val sexp_of_showable : showable -> Sexplib0.Sexp.t
val showable_of_sexp : Sexplib0.Sexp.t -> showable
val showable_to_yojson : showable -> Yojson.Safe.t
val hash_fold_showable : Base.Hash.state -> showable -> Base.Hash.state
val hash_showable : showable -> Base.Hash.hash_value
val compare_showable : showable -> showable -> int
type comment = Vernacexpr.comment =
  1. | CommentConstr of Constrexpr.constr_expr
  2. | CommentString of string
  3. | CommentInt of int
val sexp_of_comment : comment -> Sexplib0.Sexp.t
val comment_of_sexp : Sexplib0.Sexp.t -> comment
val comment_to_yojson : comment -> Yojson.Safe.t
val hash_fold_comment : Base.Hash.state -> comment -> Base.Hash.state
val hash_comment : comment -> Base.Hash.hash_value
val compare_comment : comment -> comment -> int
type 'a search_restriction = 'a Vernacexpr.search_restriction =
  1. | SearchInside of 'a
  2. | SearchOutside of 'a
val sexp_of_search_restriction : ('a -> Sexplib0.Sexp.t) -> 'a search_restriction -> Sexplib0.Sexp.t
val search_restriction_of_sexp : (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a search_restriction
val search_restriction_to_yojson : ('a -> Yojson.Safe.t) -> 'a search_restriction -> Yojson.Safe.t
val hash_fold_search_restriction : (Base.Hash.state -> 'a -> Base.Hash.state) -> Base.Hash.state -> 'a search_restriction -> Base.Hash.state
val compare_search_restriction : ('a -> 'a -> int) -> 'a search_restriction -> 'a search_restriction -> int
type verbose_flag = bool
val sexp_of_verbose_flag : verbose_flag -> Sexplib0.Sexp.t
val verbose_flag_of_sexp : Sexplib0.Sexp.t -> verbose_flag
val verbose_flag_to_yojson : verbose_flag -> Yojson.Safe.t
val hash_fold_verbose_flag : Base.Hash.state -> verbose_flag -> Base.Hash.state
val hash_verbose_flag : verbose_flag -> Base.Hash.hash_value
val compare_verbose_flag : verbose_flag -> verbose_flag -> int
type coercion_flag = Vernacexpr.coercion_flag =
  1. | AddCoercion
  2. | NoCoercion
val sexp_of_coercion_flag : coercion_flag -> Sexplib0.Sexp.t
val coercion_flag_of_sexp : Sexplib0.Sexp.t -> coercion_flag
val coercion_flag_to_yojson : coercion_flag -> Yojson.Safe.t
val hash_fold_coercion_flag : Base.Hash.state -> coercion_flag -> Base.Hash.state
val hash_coercion_flag : coercion_flag -> Base.Hash.hash_value
val compare_coercion_flag : coercion_flag -> coercion_flag -> int
type instance_flag = Vernacexpr.instance_flag =
  1. | BackInstance
  2. | BackInstanceWarning
  3. | NoInstance
val sexp_of_instance_flag : instance_flag -> Sexplib0.Sexp.t
val instance_flag_of_sexp : Sexplib0.Sexp.t -> instance_flag
val instance_flag_to_yojson : instance_flag -> Yojson.Safe.t
val hash_fold_instance_flag : Base.Hash.state -> instance_flag -> Base.Hash.state
val hash_instance_flag : instance_flag -> Base.Hash.hash_value
val compare_instance_flag : instance_flag -> instance_flag -> int
type export_flag = Lib.export_flag =
  1. | Export
  2. | Import
val sexp_of_export_flag : export_flag -> Sexplib0.Sexp.t
val export_flag_of_sexp : Sexplib0.Sexp.t -> export_flag
val export_flag_to_yojson : export_flag -> Yojson.Safe.t
val hash_fold_export_flag : Base.Hash.state -> export_flag -> Base.Hash.state
val hash_export_flag : export_flag -> Base.Hash.hash_value
val compare_export_flag : export_flag -> export_flag -> int
type locality_flag = bool
val sexp_of_locality_flag : locality_flag -> Sexplib0.Sexp.t
val locality_flag_of_sexp : Sexplib0.Sexp.t -> locality_flag
val locality_flag_to_yojson : locality_flag -> Yojson.Safe.t
val hash_fold_locality_flag : Base.Hash.state -> locality_flag -> Base.Hash.state
val hash_locality_flag : locality_flag -> Base.Hash.hash_value
val compare_locality_flag : locality_flag -> locality_flag -> int
val sexp_of_definition_expr : definition_expr -> Sexplib0.Sexp.t
val definition_expr_of_sexp : Sexplib0.Sexp.t -> definition_expr
val definition_expr_to_yojson : definition_expr -> Yojson.Safe.t
val hash_fold_definition_expr : Base.Hash.state -> definition_expr -> Base.Hash.state
val hash_definition_expr : definition_expr -> Base.Hash.hash_value
val compare_definition_expr : definition_expr -> definition_expr -> int
type notation_declaration = Vernacexpr.notation_declaration = {
  1. ntn_decl_string : Names.lstring;
  2. ntn_decl_interp : Constrexpr.constr_expr;
  3. ntn_decl_scope : scope_name option;
  4. ntn_decl_modifiers : syntax_modifier CAst.t list;
}
val sexp_of_notation_declaration : notation_declaration -> Sexplib0.Sexp.t
val notation_declaration_of_sexp : Sexplib0.Sexp.t -> notation_declaration
val notation_declaration_to_yojson : notation_declaration -> Yojson.Safe.t
val hash_fold_notation_declaration : Base.Hash.state -> notation_declaration -> Base.Hash.state
val hash_notation_declaration : notation_declaration -> Base.Hash.hash_value
val compare_notation_declaration : notation_declaration -> notation_declaration -> int
type 'a fix_expr_gen = 'a Vernacexpr.fix_expr_gen = {
  1. fname : Names.lident;
  2. univs : Constrexpr.universe_decl_expr option;
  3. rec_order : 'a;
  4. binders : Constrexpr.local_binder_expr list;
  5. rtype : Constrexpr.constr_expr;
  6. body_def : Constrexpr.constr_expr option;
  7. notations : notation_declaration list;
}
val sexp_of_fix_expr_gen : ('a -> Sexplib0.Sexp.t) -> 'a fix_expr_gen -> Sexplib0.Sexp.t
val fix_expr_gen_of_sexp : (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a fix_expr_gen
val fix_expr_gen_to_yojson : ('a -> Yojson.Safe.t) -> 'a fix_expr_gen -> Yojson.Safe.t
val hash_fold_fix_expr_gen : (Base.Hash.state -> 'a -> Base.Hash.state) -> Base.Hash.state -> 'a fix_expr_gen -> Base.Hash.state
val compare_fix_expr_gen : ('a -> 'a -> int) -> 'a fix_expr_gen -> 'a fix_expr_gen -> int
type fixpoint_expr = Constrexpr.recursion_order_expr option fix_expr_gen
val sexp_of_fixpoint_expr : fixpoint_expr -> Sexplib0.Sexp.t
val fixpoint_expr_of_sexp : Sexplib0.Sexp.t -> fixpoint_expr
val fixpoint_expr_to_yojson : fixpoint_expr -> Yojson.Safe.t
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 = unit fix_expr_gen
val sexp_of_cofixpoint_expr : cofixpoint_expr -> Sexplib0.Sexp.t
val cofixpoint_expr_of_sexp : Sexplib0.Sexp.t -> cofixpoint_expr
val cofixpoint_expr_to_yojson : cofixpoint_expr -> Yojson.Safe.t
val hash_fold_cofixpoint_expr : Base.Hash.state -> cofixpoint_expr -> Base.Hash.state
val hash_cofixpoint_expr : cofixpoint_expr -> Base.Hash.hash_value
val compare_cofixpoint_expr : cofixpoint_expr -> cofixpoint_expr -> int
val sexp_of_local_decl_expr : local_decl_expr -> Sexplib0.Sexp.t
val local_decl_expr_of_sexp : Sexplib0.Sexp.t -> local_decl_expr
val local_decl_expr_to_yojson : local_decl_expr -> Yojson.Safe.t
val hash_fold_local_decl_expr : Base.Hash.state -> local_decl_expr -> Base.Hash.state
val hash_local_decl_expr : local_decl_expr -> Base.Hash.hash_value
val compare_local_decl_expr : local_decl_expr -> local_decl_expr -> int
type inductive_kind = Vernacexpr.inductive_kind =
  1. | Inductive_kw
  2. | CoInductive
  3. | Variant
  4. | Record
  5. | Structure
  6. | Class of bool
val sexp_of_inductive_kind : inductive_kind -> Sexplib0.Sexp.t
val inductive_kind_of_sexp : Sexplib0.Sexp.t -> inductive_kind
val inductive_kind_to_yojson : inductive_kind -> Yojson.Safe.t
val hash_fold_inductive_kind : Base.Hash.state -> inductive_kind -> Base.Hash.state
val hash_inductive_kind : inductive_kind -> Base.Hash.hash_value
val compare_inductive_kind : inductive_kind -> inductive_kind -> int
type simple_binder = Names.lident list * Constrexpr.constr_expr
val sexp_of_simple_binder : simple_binder -> Sexplib0.Sexp.t
val simple_binder_of_sexp : Sexplib0.Sexp.t -> simple_binder
val simple_binder_to_yojson : simple_binder -> Yojson.Safe.t
val hash_fold_simple_binder : Base.Hash.state -> simple_binder -> Base.Hash.state
val hash_simple_binder : simple_binder -> Base.Hash.hash_value
val compare_simple_binder : simple_binder -> simple_binder -> int
type class_binder = Names.lident * Constrexpr.constr_expr list
val sexp_of_class_binder : class_binder -> Sexplib0.Sexp.t
val class_binder_of_sexp : Sexplib0.Sexp.t -> class_binder
val class_binder_to_yojson : class_binder -> Yojson.Safe.t
val hash_fold_class_binder : Base.Hash.state -> class_binder -> Base.Hash.state
val hash_class_binder : class_binder -> Base.Hash.hash_value
val compare_class_binder : class_binder -> class_binder -> int
type 'a with_coercion = coercion_flag * 'a
val sexp_of_with_coercion : ('a -> Sexplib0.Sexp.t) -> 'a with_coercion -> Sexplib0.Sexp.t
val with_coercion_of_sexp : (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a with_coercion
val with_coercion_to_yojson : ('a -> Yojson.Safe.t) -> 'a with_coercion -> Yojson.Safe.t
val hash_fold_with_coercion : (Base.Hash.state -> 'a -> Base.Hash.state) -> Base.Hash.state -> 'a with_coercion -> Base.Hash.state
val compare_with_coercion : ('a -> 'a -> int) -> 'a with_coercion -> 'a with_coercion -> int
type 'a with_coercion_instance = (Attributes.vernac_flags * coercion_flag * instance_flag) * 'a
val sexp_of_with_coercion_instance : ('a -> Sexplib0.Sexp.t) -> 'a with_coercion_instance -> Sexplib0.Sexp.t
val with_coercion_instance_of_sexp : (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a with_coercion_instance
val with_coercion_instance_to_yojson : ('a -> Yojson.Safe.t) -> 'a with_coercion_instance -> Yojson.Safe.t
val hash_fold_with_coercion_instance : (Base.Hash.state -> 'a -> Base.Hash.state) -> Base.Hash.state -> 'a with_coercion_instance -> Base.Hash.state
val compare_with_coercion_instance : ('a -> 'a -> int) -> 'a with_coercion_instance -> 'a with_coercion_instance -> int
val sexp_of_constructor_expr : constructor_expr -> Sexplib0.Sexp.t
val constructor_expr_of_sexp : Sexplib0.Sexp.t -> constructor_expr
val constructor_expr_to_yojson : constructor_expr -> Yojson.Safe.t
val hash_fold_constructor_expr : Base.Hash.state -> constructor_expr -> Base.Hash.state
val hash_constructor_expr : constructor_expr -> Base.Hash.hash_value
val compare_constructor_expr : constructor_expr -> constructor_expr -> int
type record_field_attr_unparsed = Vernacexpr.record_field_attr_unparsed = {
  1. rfu_attrs : Attributes.vernac_flags;
  2. rfu_coercion : coercion_flag;
  3. rfu_instance : instance_flag;
  4. rfu_priority : int option;
  5. rfu_notation : notation_declaration list;
}
val sexp_of_record_field_attr_unparsed : record_field_attr_unparsed -> Sexplib0.Sexp.t
val record_field_attr_unparsed_of_sexp : Sexplib0.Sexp.t -> record_field_attr_unparsed
val record_field_attr_unparsed_to_yojson : record_field_attr_unparsed -> Yojson.Safe.t
val hash_fold_record_field_attr_unparsed : Base.Hash.state -> record_field_attr_unparsed -> Base.Hash.state
val hash_record_field_attr_unparsed : record_field_attr_unparsed -> Base.Hash.hash_value
val compare_record_field_attr_unparsed : record_field_attr_unparsed -> record_field_attr_unparsed -> int
type constructor_list_or_record_decl_expr = Vernacexpr.constructor_list_or_record_decl_expr =
  1. | Constructors of constructor_expr list
  2. | RecordDecl of Names.lident option * (local_decl_expr * record_field_attr_unparsed) list * Names.lident option
val sexp_of_constructor_list_or_record_decl_expr : constructor_list_or_record_decl_expr -> Sexplib0.Sexp.t
val constructor_list_or_record_decl_expr_of_sexp : Sexplib0.Sexp.t -> constructor_list_or_record_decl_expr
val constructor_list_or_record_decl_expr_to_yojson : constructor_list_or_record_decl_expr -> Yojson.Safe.t
val constructor_list_or_record_decl_expr_of_yojson : Yojson.Safe.t -> constructor_list_or_record_decl_expr Ppx_deriving_yojson_runtime.error_or
val hash_fold_constructor_list_or_record_decl_expr : Base.Hash.state -> constructor_list_or_record_decl_expr -> Base.Hash.state
val hash_constructor_list_or_record_decl_expr : constructor_list_or_record_decl_expr -> Base.Hash.hash_value
val compare_constructor_list_or_record_decl_expr : constructor_list_or_record_decl_expr -> constructor_list_or_record_decl_expr -> int
type inductive_params_expr = Constrexpr.local_binder_expr list * Constrexpr.local_binder_expr list option
val sexp_of_inductive_params_expr : inductive_params_expr -> Sexplib0.Sexp.t
val inductive_params_expr_of_sexp : Sexplib0.Sexp.t -> inductive_params_expr
val inductive_params_expr_to_yojson : inductive_params_expr -> Yojson.Safe.t
val hash_fold_inductive_params_expr : Base.Hash.state -> inductive_params_expr -> Base.Hash.state
val hash_inductive_params_expr : inductive_params_expr -> Base.Hash.hash_value
val compare_inductive_params_expr : inductive_params_expr -> inductive_params_expr -> int
val sexp_of_inductive_expr : inductive_expr -> Sexplib0.Sexp.t
val inductive_expr_of_sexp : Sexplib0.Sexp.t -> inductive_expr
val inductive_expr_to_yojson : inductive_expr -> Yojson.Safe.t
val hash_fold_inductive_expr : Base.Hash.state -> inductive_expr -> Base.Hash.state
val hash_inductive_expr : inductive_expr -> Base.Hash.hash_value
val compare_inductive_expr : inductive_expr -> inductive_expr -> int
val sexp_of_one_inductive_expr : one_inductive_expr -> Sexplib0.Sexp.t
val one_inductive_expr_of_sexp : Sexplib0.Sexp.t -> one_inductive_expr
val one_inductive_expr_to_yojson : one_inductive_expr -> Yojson.Safe.t
val hash_fold_one_inductive_expr : Base.Hash.state -> one_inductive_expr -> Base.Hash.state
val hash_one_inductive_expr : one_inductive_expr -> Base.Hash.hash_value
val compare_one_inductive_expr : one_inductive_expr -> one_inductive_expr -> int
val sexp_of_proof_expr : proof_expr -> Sexplib0.Sexp.t
val proof_expr_of_sexp : Sexplib0.Sexp.t -> proof_expr
val proof_expr_to_yojson : proof_expr -> Yojson.Safe.t
val hash_fold_proof_expr : Base.Hash.state -> proof_expr -> Base.Hash.state
val hash_proof_expr : proof_expr -> Base.Hash.hash_value
val compare_proof_expr : proof_expr -> proof_expr -> int
type proof_end = Vernacexpr.proof_end =
  1. | Admitted
  2. | Proved of opacity_flag * Names.lident option
val sexp_of_proof_end : proof_end -> Sexplib0.Sexp.t
val proof_end_of_sexp : Sexplib0.Sexp.t -> proof_end
val proof_end_to_yojson : proof_end -> Yojson.Safe.t
val hash_fold_proof_end : Base.Hash.state -> proof_end -> Base.Hash.state
val hash_proof_end : proof_end -> Base.Hash.hash_value
val compare_proof_end : proof_end -> proof_end -> int
type scheme_type = Vernacexpr.scheme_type =
  1. | SchemeInduction
  2. | SchemeMinimality
  3. | SchemeElimination
  4. | SchemeCase
val sexp_of_scheme_type : scheme_type -> Sexplib0.Sexp.t
val scheme_type_of_sexp : Sexplib0.Sexp.t -> scheme_type
val scheme_type_to_yojson : scheme_type -> Yojson.Safe.t
val hash_fold_scheme_type : Base.Hash.state -> scheme_type -> Base.Hash.state
val hash_scheme_type : scheme_type -> Base.Hash.hash_value
val compare_scheme_type : scheme_type -> scheme_type -> int
type scheme = Vernacexpr.scheme = {
  1. sch_type : scheme_type;
  2. sch_qualid : Libnames.qualid Constrexpr.or_by_notation;
  3. sch_sort : Sorts.family;
}
val sexp_of_scheme : scheme -> Sexplib0.Sexp.t
val scheme_of_sexp : Sexplib0.Sexp.t -> scheme
val scheme_to_yojson : scheme -> Yojson.Safe.t
val hash_fold_scheme : Base.Hash.state -> scheme -> Base.Hash.state
val hash_scheme : scheme -> Base.Hash.hash_value
val compare_scheme : scheme -> scheme -> int
type section_subset_expr = Vernacexpr.section_subset_expr =
  1. | SsEmpty
  2. | SsType
  3. | SsSingl of Names.lident
  4. | SsCompl of section_subset_expr
  5. | SsUnion of section_subset_expr * section_subset_expr
  6. | SsSubstr of section_subset_expr * section_subset_expr
  7. | SsFwdClose of section_subset_expr
val sexp_of_section_subset_expr : section_subset_expr -> Sexplib0.Sexp.t
val section_subset_expr_of_sexp : Sexplib0.Sexp.t -> section_subset_expr
val section_subset_expr_to_yojson : section_subset_expr -> Yojson.Safe.t
val hash_fold_section_subset_expr : Base.Hash.state -> section_subset_expr -> Base.Hash.state
val hash_section_subset_expr : section_subset_expr -> Base.Hash.hash_value
val compare_section_subset_expr : section_subset_expr -> section_subset_expr -> int
type extend_name = Vernacexpr.extend_name = {
  1. ext_plugin : string;
  2. ext_entry : string;
  3. ext_index : int;
}
val sexp_of_extend_name : extend_name -> Sexplib0.Sexp.t
val extend_name_of_sexp : Sexplib0.Sexp.t -> extend_name
val extend_name_to_yojson : extend_name -> Yojson.Safe.t
val hash_fold_extend_name : Base.Hash.state -> extend_name -> Base.Hash.state
val hash_extend_name : extend_name -> Base.Hash.hash_value
val compare_extend_name : extend_name -> extend_name -> int
type register_kind = Vernacexpr.register_kind =
  1. | RegisterInline
  2. | RegisterCoqlib of Libnames.qualid
  3. | RegisterScheme of {
    1. inductive : Libnames.qualid;
    2. scheme_kind : Libnames.qualid;
    }
val sexp_of_register_kind : register_kind -> Sexplib0.Sexp.t
val register_kind_of_sexp : Sexplib0.Sexp.t -> register_kind
val register_kind_to_yojson : register_kind -> Yojson.Safe.t
val hash_fold_register_kind : Base.Hash.state -> register_kind -> Base.Hash.state
val hash_register_kind : register_kind -> Base.Hash.hash_value
val compare_register_kind : register_kind -> register_kind -> int
val sexp_of_module_ast_inl : module_ast_inl -> Sexplib0.Sexp.t
val module_ast_inl_of_sexp : Sexplib0.Sexp.t -> module_ast_inl
val module_ast_inl_to_yojson : module_ast_inl -> Yojson.Safe.t
val hash_fold_module_ast_inl : Base.Hash.state -> module_ast_inl -> Base.Hash.state
val hash_module_ast_inl : module_ast_inl -> Base.Hash.hash_value
val compare_module_ast_inl : module_ast_inl -> module_ast_inl -> int
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 hash_fold_discharge : Base.Hash.state -> discharge -> Base.Hash.state
val hash_discharge : discharge -> Base.Hash.hash_value
val compare_discharge : discharge -> discharge -> int
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 hash_fold_equality_scheme_type : Base.Hash.state -> equality_scheme_type -> Base.Hash.state
val hash_equality_scheme_type : equality_scheme_type -> Base.Hash.hash_value
val compare_equality_scheme_type : equality_scheme_type -> equality_scheme_type -> int
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 hash_fold_import_categories : Base.Hash.state -> import_categories -> Base.Hash.state
val hash_import_categories : import_categories -> Base.Hash.hash_value
val compare_import_categories : import_categories -> import_categories -> int
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 hash_fold_export_with_cats : Base.Hash.state -> export_with_cats -> Base.Hash.state
val hash_export_with_cats : export_with_cats -> Base.Hash.hash_value
val compare_export_with_cats : export_with_cats -> export_with_cats -> int
type module_binder = export_with_cats option * Names.lident list * module_ast_inl
val sexp_of_module_binder : module_binder -> Sexplib0.Sexp.t
val module_binder_of_sexp : Sexplib0.Sexp.t -> module_binder
val module_binder_to_yojson : module_binder -> Yojson.Safe.t
val hash_fold_module_binder : Base.Hash.state -> module_binder -> Base.Hash.state
val hash_module_binder : module_binder -> Base.Hash.hash_value
val compare_module_binder : module_binder -> module_binder -> int
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 hash_fold_one_import_filter_name : Base.Hash.state -> one_import_filter_name -> Base.Hash.state
val hash_one_import_filter_name : one_import_filter_name -> Base.Hash.hash_value
val compare_one_import_filter_name : one_import_filter_name -> one_import_filter_name -> int
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 hash_fold_import_filter_expr : Base.Hash.state -> import_filter_expr -> Base.Hash.state
val hash_import_filter_expr : import_filter_expr -> Base.Hash.hash_value
val compare_import_filter_expr : import_filter_expr -> import_filter_expr -> int
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 hash_fold_hint_info_expr : Base.Hash.state -> hint_info_expr -> Base.Hash.state
val hash_hint_info_expr : hint_info_expr -> Base.Hash.hash_value
val compare_hint_info_expr : hint_info_expr -> hint_info_expr -> int
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 hash_fold_reference_or_constr : Base.Hash.state -> reference_or_constr -> Base.Hash.state
val hash_reference_or_constr : reference_or_constr -> Base.Hash.hash_value
val compare_reference_or_constr : reference_or_constr -> reference_or_constr -> int
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 hash_fold_hints_expr : Base.Hash.state -> hints_expr -> Base.Hash.state
val hash_hints_expr : hints_expr -> Base.Hash.hash_value
val compare_hints_expr : hints_expr -> hints_expr -> int
type vernac_one_argument_status = Vernacexpr.vernac_one_argument_status = {
  1. name : Names.Name.t;
  2. recarg_like : bool;
  3. notation_scope : scope_delimiter 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 hash_fold_vernac_one_argument_status : Base.Hash.state -> vernac_one_argument_status -> Base.Hash.state
val hash_vernac_one_argument_status : vernac_one_argument_status -> Base.Hash.hash_value
val compare_vernac_one_argument_status : vernac_one_argument_status -> vernac_one_argument_status -> int
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 hash_fold_vernac_argument_status : Base.Hash.state -> vernac_argument_status -> Base.Hash.state
val hash_vernac_argument_status : vernac_argument_status -> Base.Hash.hash_value
val compare_vernac_argument_status : vernac_argument_status -> vernac_argument_status -> int
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 hash_fold_arguments_modifier : Base.Hash.state -> arguments_modifier -> Base.Hash.state
val hash_arguments_modifier : arguments_modifier -> Base.Hash.hash_value
val compare_arguments_modifier : arguments_modifier -> arguments_modifier -> int
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 hash_fold_option_setting : Base.Hash.state -> option_setting -> Base.Hash.state
val hash_option_setting : option_setting -> Base.Hash.hash_value
val compare_option_setting : option_setting -> option_setting -> int
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 hash_fold_notation_enable_modifier : Base.Hash.state -> notation_enable_modifier -> Base.Hash.state
val hash_notation_enable_modifier : notation_enable_modifier -> Base.Hash.hash_value
val compare_notation_enable_modifier : notation_enable_modifier -> notation_enable_modifier -> int
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 hash_fold_synterp_vernac_expr : Base.Hash.state -> synterp_vernac_expr -> Base.Hash.state
val hash_synterp_vernac_expr : synterp_vernac_expr -> Base.Hash.hash_value
val compare_synterp_vernac_expr : synterp_vernac_expr -> synterp_vernac_expr -> int
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. | VernacSymbol of (Constrexpr.ident_decl list * Constrexpr.constr_expr) with_coercion list
  12. | VernacInductive of inductive_kind * (inductive_expr * notation_declaration list) list
  13. | VernacFixpoint of discharge * fixpoint_expr list
  14. | VernacCoFixpoint of discharge * cofixpoint_expr list
  15. | VernacScheme of (Names.lident option * scheme) list
  16. | VernacSchemeEquality of equality_scheme_type * Libnames.qualid Constrexpr.or_by_notation
  17. | VernacCombinedScheme of Names.lident * Names.lident list
  18. | VernacUniverse of Names.lident list
  19. | VernacConstraint of Constrexpr.univ_constraint_expr list
  20. | VernacAddRewRule of Names.lident * (Constrexpr.universe_decl_expr option * Constrexpr.constr_expr * Constrexpr.constr_expr) list
  21. | VernacCanonical of Libnames.qualid Constrexpr.or_by_notation
  22. | VernacCoercion of Libnames.qualid Constrexpr.or_by_notation * (coercion_class * coercion_class) option
  23. | VernacIdentityCoercion of Names.lident * coercion_class * coercion_class
  24. | VernacNameSectionHypSet of Names.lident * section_subset_expr
  25. | VernacInstance of Constrexpr.name_decl * Constrexpr.local_binder_expr list * Constrexpr.constr_expr * (bool * Constrexpr.constr_expr) option * hint_info_expr
  26. | VernacDeclareInstance of Constrexpr.ident_decl * Constrexpr.local_binder_expr list * Constrexpr.constr_expr * hint_info_expr
  27. | VernacContext of Constrexpr.local_binder_expr list
  28. | VernacExistingInstance of (Libnames.qualid * hint_info_expr) list
  29. | VernacExistingClass of Libnames.qualid
  30. | VernacResetName of Names.lident
  31. | VernacResetInitial
  32. | VernacBack of int
  33. | VernacCreateHintDb of string * bool
  34. | VernacRemoveHints of string list * Libnames.qualid list
  35. | VernacHints of string list * hints_expr
  36. | VernacSyntacticDefinition of Names.lident * Names.Id.t list * Constrexpr.constr_expr * syntax_modifier CAst.t list
  37. | VernacArguments of Libnames.qualid Constrexpr.or_by_notation * vernac_argument_status list * (Names.Name.t * Glob_term.binding_kind) list list * arguments_modifier list
  38. | VernacReserve of simple_binder list
  39. | VernacGeneralizable of Names.lident list option
  40. | VernacSetOpacity of Conv_oracle.level * Libnames.qualid Constrexpr.or_by_notation list * bool
  41. | VernacSetStrategy of (Conv_oracle.level * Libnames.qualid Constrexpr.or_by_notation list) list
  42. | VernacMemOption of Goptions.option_name * Goptions.table_value list
  43. | VernacPrintOption of Goptions.option_name
  44. | VernacCheckMayEval of Genredexpr.raw_red_expr option * Goal_select.t option * Constrexpr.constr_expr
  45. | VernacGlobalCheck of Constrexpr.constr_expr
  46. | VernacDeclareReduction of string * Genredexpr.raw_red_expr
  47. | VernacPrint of printable
  48. | VernacSearch of searchable * Goal_select.t option * Libnames.qualid list search_restriction
  49. | VernacLocate of locatable
  50. | VernacRegister of Libnames.qualid * register_kind
  51. | VernacPrimitive of Constrexpr.ident_decl * CPrimitives.op_or_type * Constrexpr.constr_expr option
  52. | VernacComments of comment list
  53. | VernacAttributes of Attributes.vernac_flags
  54. | VernacAbort
  55. | VernacAbortAll
  56. | VernacRestart
  57. | VernacUndo of int
  58. | VernacUndoTo of int
  59. | VernacFocus of int option
  60. | VernacUnfocus
  61. | VernacUnfocused
  62. | VernacBullet of Proof_bullet.t
  63. | VernacSubproof of Goal_select.t option
  64. | VernacEndSubproof
  65. | VernacShow of showable
  66. | VernacCheckGuard
  67. | VernacValidateProof
  68. | VernacProof of Genarg.raw_generic_argument option * section_subset_expr option
  69. | VernacAddOption of Goptions.option_name * Goptions.table_value list
  70. | 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 hash_fold_synpure_vernac_expr : Base.Hash.state -> synpure_vernac_expr -> Base.Hash.state
val hash_synpure_vernac_expr : synpure_vernac_expr -> Base.Hash.hash_value
val compare_synpure_vernac_expr : synpure_vernac_expr -> synpure_vernac_expr -> int
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 hash_fold_vernac_expr_gen : (Base.Hash.state -> 'a -> Base.Hash.state) -> Base.Hash.state -> 'a vernac_expr_gen -> Base.Hash.state
val compare_vernac_expr_gen : ('a -> 'a -> int) -> 'a vernac_expr_gen -> 'a vernac_expr_gen -> int
type control_flag = Vernacexpr.control_flag =
  1. | ControlTime
  2. | ControlInstructions
  3. | ControlRedirect of string
  4. | ControlTimeout of int
  5. | ControlFail
  6. | 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 hash_fold_control_flag : Base.Hash.state -> control_flag -> Base.Hash.state
val hash_control_flag : control_flag -> Base.Hash.hash_value
val compare_control_flag : control_flag -> control_flag -> int
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 hash_fold_vernac_control_gen_r : (Base.Hash.state -> 'a -> Base.Hash.state) -> (Base.Hash.state -> 'b -> Base.Hash.state) -> Base.Hash.state -> ('a, 'b) vernac_control_gen_r -> Base.Hash.state
val compare_vernac_control_gen_r : ('a -> 'a -> int) -> ('b -> 'b -> int) -> ('a, 'b) vernac_control_gen_r -> ('a, 'b) vernac_control_gen_r -> int
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 hash_fold_vernac_control_gen : (Base.Hash.state -> 'a -> Base.Hash.state) -> Base.Hash.state -> 'a vernac_control_gen -> Base.Hash.state
val compare_vernac_control_gen : ('a -> 'a -> int) -> 'a vernac_control_gen -> 'a vernac_control_gen -> int
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 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.

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