package coq-serapi

  1. Overview
  2. Docs
package coq-serapi
Legend:
Library
Module
Module type
Parameter
Class
Class type
type infix_flag = bool
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
val sexp_of_infix_flag : infix_flag -> Sexplib0.Sexp.t
val infix_flag_of_sexp : Sexplib0.Sexp.t -> infix_flag
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 opacity_flag_to_yojson : opacity_flag -> Yojson.Safe.t
val opacity_flag_of_yojson : Yojson.Safe.t -> opacity_flag Ppx_deriving_yojson_runtime.error_or
val sexp_of_opacity_flag : opacity_flag -> Sexplib0.Sexp.t
val opacity_flag_of_sexp : Sexplib0.Sexp.t -> opacity_flag
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 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
val sexp_of_scope_name : scope_name -> Sexplib0.Sexp.t
val scope_name_of_sexp : Sexplib0.Sexp.t -> scope_name
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 scope_delimiter_to_yojson : scope_delimiter -> Yojson.Safe.t
val scope_delimiter_of_yojson : Yojson.Safe.t -> scope_delimiter Ppx_deriving_yojson_runtime.error_or
val sexp_of_scope_delimiter : scope_delimiter -> Sexplib0.Sexp.t
val scope_delimiter_of_sexp : Sexplib0.Sexp.t -> scope_delimiter
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 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
val sexp_of_notation_format : notation_format -> Sexplib0.Sexp.t
val notation_format_of_sexp : Sexplib0.Sexp.t -> notation_format
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 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
val sexp_of_syntax_modifier : syntax_modifier -> Sexplib0.Sexp.t
val syntax_modifier_of_sexp : Sexplib0.Sexp.t -> syntax_modifier
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 coercion_class_to_yojson : coercion_class -> Yojson.Safe.t
val coercion_class_of_yojson : Yojson.Safe.t -> coercion_class Ppx_deriving_yojson_runtime.error_or
val sexp_of_coercion_class : coercion_class -> Sexplib0.Sexp.t
val coercion_class_of_sexp : Sexplib0.Sexp.t -> coercion_class
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 goal_reference_to_yojson : goal_reference -> Yojson.Safe.t
val goal_reference_of_yojson : Yojson.Safe.t -> goal_reference Ppx_deriving_yojson_runtime.error_or
val sexp_of_goal_reference : goal_reference -> Sexplib0.Sexp.t
val goal_reference_of_sexp : Sexplib0.Sexp.t -> goal_reference
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. | PrintNotation of Constrexpr.notation_entry * string
val printable_to_yojson : printable -> Yojson.Safe.t
val printable_of_yojson : Yojson.Safe.t -> printable Ppx_deriving_yojson_runtime.error_or
val sexp_of_printable : printable -> Sexplib0.Sexp.t
val printable_of_sexp : Sexplib0.Sexp.t -> printable
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 glob_search_where_to_yojson : glob_search_where -> Yojson.Safe.t
val glob_search_where_of_yojson : Yojson.Safe.t -> glob_search_where Ppx_deriving_yojson_runtime.error_or
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 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 search_item_to_yojson : search_item -> Yojson.Safe.t
val search_item_of_yojson : Yojson.Safe.t -> search_item Ppx_deriving_yojson_runtime.error_or
val sexp_of_search_item : search_item -> Sexplib0.Sexp.t
val search_item_of_sexp : Sexplib0.Sexp.t -> search_item
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 search_request_to_yojson : search_request -> Yojson.Safe.t
val search_request_of_yojson : Yojson.Safe.t -> search_request Ppx_deriving_yojson_runtime.error_or
val sexp_of_search_request : search_request -> Sexplib0.Sexp.t
val search_request_of_sexp : Sexplib0.Sexp.t -> search_request
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 searchable_to_yojson : searchable -> Yojson.Safe.t
val searchable_of_yojson : Yojson.Safe.t -> searchable Ppx_deriving_yojson_runtime.error_or
val sexp_of_searchable : searchable -> Sexplib0.Sexp.t
val searchable_of_sexp : Sexplib0.Sexp.t -> searchable
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 locatable_to_yojson : locatable -> Yojson.Safe.t
val locatable_of_yojson : Yojson.Safe.t -> locatable Ppx_deriving_yojson_runtime.error_or
val sexp_of_locatable : locatable -> Sexplib0.Sexp.t
val locatable_of_sexp : Sexplib0.Sexp.t -> locatable
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 showable_to_yojson : showable -> Yojson.Safe.t
val showable_of_yojson : Yojson.Safe.t -> showable Ppx_deriving_yojson_runtime.error_or
val sexp_of_showable : showable -> Sexplib0.Sexp.t
val showable_of_sexp : Sexplib0.Sexp.t -> showable
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 comment_to_yojson : comment -> Yojson.Safe.t
val comment_of_yojson : Yojson.Safe.t -> comment Ppx_deriving_yojson_runtime.error_or
val sexp_of_comment : comment -> Sexplib0.Sexp.t
val comment_of_sexp : Sexplib0.Sexp.t -> comment
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 search_restriction_to_yojson : ('a -> Yojson.Safe.t) -> 'a search_restriction -> Yojson.Safe.t
val search_restriction_of_yojson : (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) -> Yojson.Safe.t -> 'a search_restriction Ppx_deriving_yojson_runtime.error_or
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 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 verbose_flag_to_yojson : verbose_flag -> Yojson.Safe.t
val verbose_flag_of_yojson : Yojson.Safe.t -> verbose_flag Ppx_deriving_yojson_runtime.error_or
val sexp_of_verbose_flag : verbose_flag -> Sexplib0.Sexp.t
val verbose_flag_of_sexp : Sexplib0.Sexp.t -> verbose_flag
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 coercion_flag_to_yojson : coercion_flag -> Yojson.Safe.t
val coercion_flag_of_yojson : Yojson.Safe.t -> coercion_flag Ppx_deriving_yojson_runtime.error_or
val sexp_of_coercion_flag : coercion_flag -> Sexplib0.Sexp.t
val coercion_flag_of_sexp : Sexplib0.Sexp.t -> coercion_flag
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 instance_flag_to_yojson : instance_flag -> Yojson.Safe.t
val instance_flag_of_yojson : Yojson.Safe.t -> instance_flag Ppx_deriving_yojson_runtime.error_or
val sexp_of_instance_flag : instance_flag -> Sexplib0.Sexp.t
val instance_flag_of_sexp : Sexplib0.Sexp.t -> instance_flag
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 export_flag_to_yojson : export_flag -> Yojson.Safe.t
val export_flag_of_yojson : Yojson.Safe.t -> export_flag Ppx_deriving_yojson_runtime.error_or
val sexp_of_export_flag : export_flag -> Sexplib0.Sexp.t
val export_flag_of_sexp : Sexplib0.Sexp.t -> export_flag
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 locality_flag_to_yojson : locality_flag -> Yojson.Safe.t
val locality_flag_of_yojson : Yojson.Safe.t -> locality_flag Ppx_deriving_yojson_runtime.error_or
val sexp_of_locality_flag : locality_flag -> Sexplib0.Sexp.t
val locality_flag_of_sexp : Sexplib0.Sexp.t -> locality_flag
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 definition_expr_to_yojson : definition_expr -> Yojson.Safe.t
val definition_expr_of_yojson : Yojson.Safe.t -> definition_expr Ppx_deriving_yojson_runtime.error_or
val sexp_of_definition_expr : definition_expr -> Sexplib0.Sexp.t
val definition_expr_of_sexp : Sexplib0.Sexp.t -> definition_expr
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 notation_declaration_to_yojson : notation_declaration -> Yojson.Safe.t
val notation_declaration_of_yojson : Yojson.Safe.t -> notation_declaration Ppx_deriving_yojson_runtime.error_or
val sexp_of_notation_declaration : notation_declaration -> Sexplib0.Sexp.t
val notation_declaration_of_sexp : Sexplib0.Sexp.t -> notation_declaration
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 fix_expr_gen_to_yojson : ('a -> Yojson.Safe.t) -> 'a fix_expr_gen -> Yojson.Safe.t
val fix_expr_gen_of_yojson : (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) -> Yojson.Safe.t -> 'a fix_expr_gen Ppx_deriving_yojson_runtime.error_or
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 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 fixpoint_expr_to_yojson : fixpoint_expr -> Yojson.Safe.t
val fixpoint_expr_of_yojson : Yojson.Safe.t -> fixpoint_expr Ppx_deriving_yojson_runtime.error_or
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 = unit fix_expr_gen
val cofixpoint_expr_to_yojson : cofixpoint_expr -> Yojson.Safe.t
val cofixpoint_expr_of_yojson : Yojson.Safe.t -> cofixpoint_expr Ppx_deriving_yojson_runtime.error_or
val sexp_of_cofixpoint_expr : cofixpoint_expr -> Sexplib0.Sexp.t
val cofixpoint_expr_of_sexp : Sexplib0.Sexp.t -> cofixpoint_expr
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 local_decl_expr_to_yojson : local_decl_expr -> Yojson.Safe.t
val local_decl_expr_of_yojson : Yojson.Safe.t -> local_decl_expr Ppx_deriving_yojson_runtime.error_or
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 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 inductive_kind_to_yojson : inductive_kind -> Yojson.Safe.t
val inductive_kind_of_yojson : Yojson.Safe.t -> inductive_kind Ppx_deriving_yojson_runtime.error_or
val sexp_of_inductive_kind : inductive_kind -> Sexplib0.Sexp.t
val inductive_kind_of_sexp : Sexplib0.Sexp.t -> inductive_kind
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 simple_binder_to_yojson : simple_binder -> Yojson.Safe.t
val simple_binder_of_yojson : Yojson.Safe.t -> simple_binder Ppx_deriving_yojson_runtime.error_or
val sexp_of_simple_binder : simple_binder -> Sexplib0.Sexp.t
val simple_binder_of_sexp : Sexplib0.Sexp.t -> simple_binder
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 class_binder_to_yojson : class_binder -> Yojson.Safe.t
val class_binder_of_yojson : Yojson.Safe.t -> class_binder Ppx_deriving_yojson_runtime.error_or
val sexp_of_class_binder : class_binder -> Sexplib0.Sexp.t
val class_binder_of_sexp : Sexplib0.Sexp.t -> class_binder
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 with_coercion_to_yojson : ('a -> Yojson.Safe.t) -> 'a with_coercion -> Yojson.Safe.t
val with_coercion_of_yojson : (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) -> Yojson.Safe.t -> 'a with_coercion Ppx_deriving_yojson_runtime.error_or
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 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 with_coercion_instance_to_yojson : ('a -> Yojson.Safe.t) -> 'a with_coercion_instance -> Yojson.Safe.t
val with_coercion_instance_of_yojson : (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) -> Yojson.Safe.t -> 'a with_coercion_instance Ppx_deriving_yojson_runtime.error_or
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 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 constructor_expr_to_yojson : constructor_expr -> Yojson.Safe.t
val constructor_expr_of_yojson : Yojson.Safe.t -> constructor_expr Ppx_deriving_yojson_runtime.error_or
val sexp_of_constructor_expr : constructor_expr -> Sexplib0.Sexp.t
val constructor_expr_of_sexp : Sexplib0.Sexp.t -> constructor_expr
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 record_field_attr_unparsed_to_yojson : record_field_attr_unparsed -> Yojson.Safe.t
val record_field_attr_unparsed_of_yojson : Yojson.Safe.t -> record_field_attr_unparsed Ppx_deriving_yojson_runtime.error_or
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 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 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 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 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 inductive_params_expr_to_yojson : inductive_params_expr -> Yojson.Safe.t
val inductive_params_expr_of_yojson : Yojson.Safe.t -> inductive_params_expr Ppx_deriving_yojson_runtime.error_or
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 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 inductive_expr_to_yojson : inductive_expr -> Yojson.Safe.t
val inductive_expr_of_yojson : Yojson.Safe.t -> inductive_expr Ppx_deriving_yojson_runtime.error_or
val sexp_of_inductive_expr : inductive_expr -> Sexplib0.Sexp.t
val inductive_expr_of_sexp : Sexplib0.Sexp.t -> inductive_expr
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 one_inductive_expr_to_yojson : one_inductive_expr -> Yojson.Safe.t
val one_inductive_expr_of_yojson : Yojson.Safe.t -> one_inductive_expr Ppx_deriving_yojson_runtime.error_or
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 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 proof_expr_to_yojson : proof_expr -> Yojson.Safe.t
val proof_expr_of_yojson : Yojson.Safe.t -> proof_expr Ppx_deriving_yojson_runtime.error_or
val sexp_of_proof_expr : proof_expr -> Sexplib0.Sexp.t
val proof_expr_of_sexp : Sexplib0.Sexp.t -> proof_expr
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 proof_end_to_yojson : proof_end -> Yojson.Safe.t
val proof_end_of_yojson : Yojson.Safe.t -> proof_end Ppx_deriving_yojson_runtime.error_or
val sexp_of_proof_end : proof_end -> Sexplib0.Sexp.t
val proof_end_of_sexp : Sexplib0.Sexp.t -> proof_end
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 scheme_type_to_yojson : scheme_type -> Yojson.Safe.t
val scheme_type_of_yojson : Yojson.Safe.t -> scheme_type Ppx_deriving_yojson_runtime.error_or
val sexp_of_scheme_type : scheme_type -> Sexplib0.Sexp.t
val scheme_type_of_sexp : Sexplib0.Sexp.t -> scheme_type
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 scheme_to_yojson : scheme -> Yojson.Safe.t
val scheme_of_yojson : Yojson.Safe.t -> scheme Ppx_deriving_yojson_runtime.error_or
val sexp_of_scheme : scheme -> Sexplib0.Sexp.t
val scheme_of_sexp : Sexplib0.Sexp.t -> scheme
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 section_subset_expr_to_yojson : section_subset_expr -> Yojson.Safe.t
val section_subset_expr_of_yojson : Yojson.Safe.t -> section_subset_expr Ppx_deriving_yojson_runtime.error_or
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 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 extend_name_to_yojson : extend_name -> Yojson.Safe.t
val extend_name_of_yojson : Yojson.Safe.t -> extend_name Ppx_deriving_yojson_runtime.error_or
val sexp_of_extend_name : extend_name -> Sexplib0.Sexp.t
val extend_name_of_sexp : Sexplib0.Sexp.t -> extend_name
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
val register_kind_to_yojson : register_kind -> Yojson.Safe.t
val register_kind_of_yojson : Yojson.Safe.t -> register_kind Ppx_deriving_yojson_runtime.error_or
val sexp_of_register_kind : register_kind -> Sexplib0.Sexp.t
val register_kind_of_sexp : Sexplib0.Sexp.t -> register_kind
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 module_ast_inl_to_yojson : module_ast_inl -> Yojson.Safe.t
val module_ast_inl_of_yojson : Yojson.Safe.t -> module_ast_inl Ppx_deriving_yojson_runtime.error_or
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 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 discharge_to_yojson : discharge -> Yojson.Safe.t
val discharge_of_yojson : Yojson.Safe.t -> discharge Ppx_deriving_yojson_runtime.error_or
val sexp_of_discharge : discharge -> Sexplib0.Sexp.t
val discharge_of_sexp : Sexplib0.Sexp.t -> discharge
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 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
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 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 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
val sexp_of_import_categories : import_categories -> Sexplib0.Sexp.t
val import_categories_of_sexp : Sexplib0.Sexp.t -> import_categories
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 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
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 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 module_binder_to_yojson : module_binder -> Yojson.Safe.t
val module_binder_of_yojson : Yojson.Safe.t -> module_binder Ppx_deriving_yojson_runtime.error_or
val sexp_of_module_binder : module_binder -> Sexplib0.Sexp.t
val module_binder_of_sexp : Sexplib0.Sexp.t -> module_binder
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 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
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 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 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
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 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 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
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 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 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
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 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 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
val sexp_of_hints_expr : hints_expr -> Sexplib0.Sexp.t
val hints_expr_of_sexp : Sexplib0.Sexp.t -> hints_expr
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 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
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 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 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
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 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 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
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 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 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
val sexp_of_option_setting : option_setting -> Sexplib0.Sexp.t
val option_setting_of_sexp : Sexplib0.Sexp.t -> option_setting
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 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
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 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 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
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 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. | 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 * Libnames.qualid list 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. | VernacAttributes of Attributes.vernac_flags
  52. | VernacAbort
  53. | VernacAbortAll
  54. | VernacRestart
  55. | VernacUndo of int
  56. | VernacUndoTo of int
  57. | VernacFocus of int option
  58. | VernacUnfocus
  59. | VernacUnfocused
  60. | VernacBullet of Proof_bullet.t
  61. | VernacSubproof of Goal_select.t option
  62. | VernacEndSubproof
  63. | VernacShow of showable
  64. | VernacCheckGuard
  65. | VernacValidateProof
  66. | VernacProof of Genarg.raw_generic_argument option * section_subset_expr option
  67. | VernacAddOption of Goptions.option_name * Goptions.table_value list
  68. | VernacRemoveOption of Goptions.option_name * Goptions.table_value list
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
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 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 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
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 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 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
val sexp_of_control_flag : control_flag -> Sexplib0.Sexp.t
val control_flag_of_sexp : Sexplib0.Sexp.t -> control_flag
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 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
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 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 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_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 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 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 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.

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