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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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