package coq-serapi

  1. Overview
  2. Docs
Serialization library and protocol for machine interaction with the Coq proof assistant

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (38)

Authors

  1. E
    Emilio Jesús Gallego Arias
  2. K
    Karl Palmskog
  3. C
    Clément Pit-Claudel
  4. K
    Kaiyu Yang

Maintainers

  1. E
    e@x80.org

Sources

coq-serapi-8.19.0.0.19.1.tbz
sha256=10d90417815073507a53dbc5cca1cf504afa58104da8557e2afa2e7daf6ec852
sha512=95006e1e2798c531a01656972990662b07db815534bc789a5f3351c7d5bc8e75156c5a3c3b3a18d37f3eab0b11ceabd17d1609ed4d8afb461698b4098106e028

doc/coq-serapi.serlib/Serlib/Ser_vernacexpr/index.html

Module Serlib.Ser_vernacexprSource

Sourcetype infix_flag = bool
Sourceval sexp_of_infix_flag : infix_flag -> Sexplib0.Sexp.t
Sourceval infix_flag_of_sexp : Sexplib0.Sexp.t -> infix_flag
Sourceval infix_flag_to_yojson : infix_flag -> Yojson.Safe.t
Sourceval hash_fold_infix_flag : Ppx_hash_lib.Std.Hash.state -> infix_flag -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_infix_flag : infix_flag -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_infix_flag : infix_flag -> infix_flag -> int
Sourcetype opacity_flag = Vernacexpr.opacity_flag =
  1. | Opaque
  2. | Transparent
Sourceval sexp_of_opacity_flag : opacity_flag -> Sexplib0.Sexp.t
Sourceval opacity_flag_of_sexp : Sexplib0.Sexp.t -> opacity_flag
Sourceval opacity_flag_to_yojson : opacity_flag -> Yojson.Safe.t
Sourceval hash_fold_opacity_flag : Ppx_hash_lib.Std.Hash.state -> opacity_flag -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_opacity_flag : opacity_flag -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_opacity_flag : opacity_flag -> opacity_flag -> int
Sourcetype scope_name = string
Sourceval sexp_of_scope_name : scope_name -> Sexplib0.Sexp.t
Sourceval scope_name_of_sexp : Sexplib0.Sexp.t -> scope_name
Sourceval scope_name_to_yojson : scope_name -> Yojson.Safe.t
Sourceval hash_fold_scope_name : Ppx_hash_lib.Std.Hash.state -> scope_name -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_scope_name : scope_name -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_scope_name : scope_name -> scope_name -> int
Sourcetype scope_delimiter = Constrexpr.delimiter_depth * scope_name
Sourceval sexp_of_scope_delimiter : scope_delimiter -> Sexplib0.Sexp.t
Sourceval scope_delimiter_of_sexp : Sexplib0.Sexp.t -> scope_delimiter
Sourceval scope_delimiter_to_yojson : scope_delimiter -> Yojson.Safe.t
Sourceval hash_fold_scope_delimiter : Ppx_hash_lib.Std.Hash.state -> scope_delimiter -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_scope_delimiter : scope_delimiter -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_scope_delimiter : scope_delimiter -> scope_delimiter -> int
Sourcetype notation_format = Vernacexpr.notation_format =
  1. | TextFormat of Names.lstring
Sourceval sexp_of_notation_format : notation_format -> Sexplib0.Sexp.t
Sourceval notation_format_of_sexp : Sexplib0.Sexp.t -> notation_format
Sourceval notation_format_to_yojson : notation_format -> Yojson.Safe.t
Sourceval hash_fold_notation_format : Ppx_hash_lib.Std.Hash.state -> notation_format -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_notation_format : notation_format -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_notation_format : notation_format -> notation_format -> int
Sourcetype 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
Sourceval sexp_of_syntax_modifier : syntax_modifier -> Sexplib0.Sexp.t
Sourceval syntax_modifier_of_sexp : Sexplib0.Sexp.t -> syntax_modifier
Sourceval syntax_modifier_to_yojson : syntax_modifier -> Yojson.Safe.t
Sourceval hash_fold_syntax_modifier : Ppx_hash_lib.Std.Hash.state -> syntax_modifier -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_syntax_modifier : syntax_modifier -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_syntax_modifier : syntax_modifier -> syntax_modifier -> int
Sourcetype coercion_class = Vernacexpr.coercion_class =
  1. | FunClass
  2. | SortClass
  3. | RefClass of Libnames.qualid Constrexpr.or_by_notation
Sourceval sexp_of_coercion_class : coercion_class -> Sexplib0.Sexp.t
Sourceval coercion_class_of_sexp : Sexplib0.Sexp.t -> coercion_class
Sourceval coercion_class_to_yojson : coercion_class -> Yojson.Safe.t
Sourceval hash_fold_coercion_class : Ppx_hash_lib.Std.Hash.state -> coercion_class -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_coercion_class : coercion_class -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_coercion_class : coercion_class -> coercion_class -> int
Sourcetype goal_reference = Vernacexpr.goal_reference =
  1. | OpenSubgoals
  2. | NthGoal of int
  3. | GoalId of Names.Id.t
Sourceval sexp_of_goal_reference : goal_reference -> Sexplib0.Sexp.t
Sourceval goal_reference_of_sexp : Sexplib0.Sexp.t -> goal_reference
Sourceval goal_reference_to_yojson : goal_reference -> Yojson.Safe.t
Sourceval hash_fold_goal_reference : Ppx_hash_lib.Std.Hash.state -> goal_reference -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_goal_reference : goal_reference -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_goal_reference : goal_reference -> goal_reference -> int
Sourcetype 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
Sourceval sexp_of_printable : printable -> Sexplib0.Sexp.t
Sourceval printable_of_sexp : Sexplib0.Sexp.t -> printable
Sourceval printable_to_yojson : printable -> Yojson.Safe.t
Sourceval hash_fold_printable : Ppx_hash_lib.Std.Hash.state -> printable -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_printable : printable -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_printable : printable -> printable -> int
Sourcetype glob_search_where = Vernacexpr.glob_search_where =
  1. | InHyp
  2. | InConcl
  3. | Anywhere
Sourceval sexp_of_glob_search_where : glob_search_where -> Sexplib0.Sexp.t
Sourceval glob_search_where_of_sexp : Sexplib0.Sexp.t -> glob_search_where
Sourceval glob_search_where_to_yojson : glob_search_where -> Yojson.Safe.t
Sourceval hash_fold_glob_search_where : Ppx_hash_lib.Std.Hash.state -> glob_search_where -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_glob_search_where : glob_search_where -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_glob_search_where : glob_search_where -> glob_search_where -> int
Sourcetype 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
Sourceval sexp_of_search_item : search_item -> Sexplib0.Sexp.t
Sourceval search_item_of_sexp : Sexplib0.Sexp.t -> search_item
Sourceval search_item_to_yojson : search_item -> Yojson.Safe.t
Sourceval hash_fold_search_item : Ppx_hash_lib.Std.Hash.state -> search_item -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_search_item : search_item -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_search_item : search_item -> search_item -> int
Sourcetype search_request = Vernacexpr.search_request =
  1. | SearchLiteral of search_item
  2. | SearchDisjConj of (bool * search_request) list list
Sourceval sexp_of_search_request : search_request -> Sexplib0.Sexp.t
Sourceval search_request_of_sexp : Sexplib0.Sexp.t -> search_request
Sourceval search_request_to_yojson : search_request -> Yojson.Safe.t
Sourceval hash_fold_search_request : Ppx_hash_lib.Std.Hash.state -> search_request -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_search_request : search_request -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_search_request : search_request -> search_request -> int
Sourcetype searchable = Vernacexpr.searchable =
  1. | SearchPattern of Constrexpr.constr_pattern_expr
  2. | SearchRewrite of Constrexpr.constr_pattern_expr
  3. | Search of (bool * search_request) list
Sourceval sexp_of_searchable : searchable -> Sexplib0.Sexp.t
Sourceval searchable_of_sexp : Sexplib0.Sexp.t -> searchable
Sourceval searchable_to_yojson : searchable -> Yojson.Safe.t
Sourceval hash_fold_searchable : Ppx_hash_lib.Std.Hash.state -> searchable -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_searchable : searchable -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_searchable : searchable -> searchable -> int
Sourcetype 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
Sourceval sexp_of_locatable : locatable -> Sexplib0.Sexp.t
Sourceval locatable_of_sexp : Sexplib0.Sexp.t -> locatable
Sourceval locatable_to_yojson : locatable -> Yojson.Safe.t
Sourceval hash_fold_locatable : Ppx_hash_lib.Std.Hash.state -> locatable -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_locatable : locatable -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_locatable : locatable -> locatable -> int
Sourcetype 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
Sourceval sexp_of_showable : showable -> Sexplib0.Sexp.t
Sourceval showable_of_sexp : Sexplib0.Sexp.t -> showable
Sourceval showable_to_yojson : showable -> Yojson.Safe.t
Sourceval hash_fold_showable : Ppx_hash_lib.Std.Hash.state -> showable -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_showable : showable -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_showable : showable -> showable -> int
Sourcetype comment = Vernacexpr.comment =
  1. | CommentConstr of Constrexpr.constr_expr
  2. | CommentString of string
  3. | CommentInt of int
Sourceval sexp_of_comment : comment -> Sexplib0.Sexp.t
Sourceval comment_of_sexp : Sexplib0.Sexp.t -> comment
Sourceval comment_to_yojson : comment -> Yojson.Safe.t
Sourceval hash_fold_comment : Ppx_hash_lib.Std.Hash.state -> comment -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_comment : comment -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_comment : comment -> comment -> int
Sourcetype 'a search_restriction = 'a Vernacexpr.search_restriction =
  1. | SearchInside of 'a
  2. | SearchOutside of 'a
Sourceval sexp_of_search_restriction : ('a -> Sexplib0.Sexp.t) -> 'a search_restriction -> Sexplib0.Sexp.t
Sourceval search_restriction_of_sexp : (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a search_restriction
Sourceval search_restriction_to_yojson : ('a -> Yojson.Safe.t) -> 'a search_restriction -> Yojson.Safe.t
Sourceval hash_fold_search_restriction : (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'a search_restriction -> Ppx_hash_lib.Std.Hash.state
Sourceval compare_search_restriction : ('a -> 'a -> int) -> 'a search_restriction -> 'a search_restriction -> int
Sourcetype verbose_flag = bool
Sourceval sexp_of_verbose_flag : verbose_flag -> Sexplib0.Sexp.t
Sourceval verbose_flag_of_sexp : Sexplib0.Sexp.t -> verbose_flag
Sourceval verbose_flag_to_yojson : verbose_flag -> Yojson.Safe.t
Sourceval hash_fold_verbose_flag : Ppx_hash_lib.Std.Hash.state -> verbose_flag -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_verbose_flag : verbose_flag -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_verbose_flag : verbose_flag -> verbose_flag -> int
Sourcetype coercion_flag = Vernacexpr.coercion_flag =
  1. | AddCoercion
  2. | NoCoercion
Sourceval sexp_of_coercion_flag : coercion_flag -> Sexplib0.Sexp.t
Sourceval coercion_flag_of_sexp : Sexplib0.Sexp.t -> coercion_flag
Sourceval coercion_flag_to_yojson : coercion_flag -> Yojson.Safe.t
Sourceval hash_fold_coercion_flag : Ppx_hash_lib.Std.Hash.state -> coercion_flag -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_coercion_flag : coercion_flag -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_coercion_flag : coercion_flag -> coercion_flag -> int
Sourcetype instance_flag = Vernacexpr.instance_flag =
  1. | BackInstance
  2. | BackInstanceWarning
  3. | NoInstance
Sourceval sexp_of_instance_flag : instance_flag -> Sexplib0.Sexp.t
Sourceval instance_flag_of_sexp : Sexplib0.Sexp.t -> instance_flag
Sourceval instance_flag_to_yojson : instance_flag -> Yojson.Safe.t
Sourceval hash_fold_instance_flag : Ppx_hash_lib.Std.Hash.state -> instance_flag -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_instance_flag : instance_flag -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_instance_flag : instance_flag -> instance_flag -> int
Sourcetype export_flag = Lib.export_flag =
  1. | Export
  2. | Import
Sourceval sexp_of_export_flag : export_flag -> Sexplib0.Sexp.t
Sourceval export_flag_of_sexp : Sexplib0.Sexp.t -> export_flag
Sourceval export_flag_to_yojson : export_flag -> Yojson.Safe.t
Sourceval hash_fold_export_flag : Ppx_hash_lib.Std.Hash.state -> export_flag -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_export_flag : export_flag -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_export_flag : export_flag -> export_flag -> int
Sourcetype locality_flag = bool
Sourceval sexp_of_locality_flag : locality_flag -> Sexplib0.Sexp.t
Sourceval locality_flag_of_sexp : Sexplib0.Sexp.t -> locality_flag
Sourceval locality_flag_to_yojson : locality_flag -> Yojson.Safe.t
Sourceval hash_fold_locality_flag : Ppx_hash_lib.Std.Hash.state -> locality_flag -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_locality_flag : locality_flag -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_locality_flag : locality_flag -> locality_flag -> int
Sourcetype definition_expr = Vernacexpr.definition_expr =
  1. | ProveBody of Constrexpr.local_binder_expr list * Constrexpr.constr_expr
  2. | DefineBody of Constrexpr.local_binder_expr list * Genredexpr.raw_red_expr option * Constrexpr.constr_expr * Constrexpr.constr_expr option
Sourceval sexp_of_definition_expr : definition_expr -> Sexplib0.Sexp.t
Sourceval definition_expr_of_sexp : Sexplib0.Sexp.t -> definition_expr
Sourceval definition_expr_to_yojson : definition_expr -> Yojson.Safe.t
Sourceval hash_fold_definition_expr : Ppx_hash_lib.Std.Hash.state -> definition_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_definition_expr : definition_expr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_definition_expr : definition_expr -> definition_expr -> int
Sourcetype 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;
}
Sourceval sexp_of_notation_declaration : notation_declaration -> Sexplib0.Sexp.t
Sourceval notation_declaration_of_sexp : Sexplib0.Sexp.t -> notation_declaration
Sourceval notation_declaration_to_yojson : notation_declaration -> Yojson.Safe.t
Sourceval hash_fold_notation_declaration : Ppx_hash_lib.Std.Hash.state -> notation_declaration -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_notation_declaration : notation_declaration -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_notation_declaration : notation_declaration -> notation_declaration -> int
Sourcetype '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;
}
Sourceval sexp_of_fix_expr_gen : ('a -> Sexplib0.Sexp.t) -> 'a fix_expr_gen -> Sexplib0.Sexp.t
Sourceval fix_expr_gen_of_sexp : (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a fix_expr_gen
Sourceval fix_expr_gen_to_yojson : ('a -> Yojson.Safe.t) -> 'a fix_expr_gen -> Yojson.Safe.t
Sourceval hash_fold_fix_expr_gen : (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'a fix_expr_gen -> Ppx_hash_lib.Std.Hash.state
Sourceval compare_fix_expr_gen : ('a -> 'a -> int) -> 'a fix_expr_gen -> 'a fix_expr_gen -> int
Sourcetype fixpoint_expr = Constrexpr.recursion_order_expr option fix_expr_gen
Sourceval sexp_of_fixpoint_expr : fixpoint_expr -> Sexplib0.Sexp.t
Sourceval fixpoint_expr_of_sexp : Sexplib0.Sexp.t -> fixpoint_expr
Sourceval fixpoint_expr_to_yojson : fixpoint_expr -> Yojson.Safe.t
Sourceval hash_fold_fixpoint_expr : Ppx_hash_lib.Std.Hash.state -> fixpoint_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_fixpoint_expr : fixpoint_expr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_fixpoint_expr : fixpoint_expr -> fixpoint_expr -> int
Sourcetype cofixpoint_expr = unit fix_expr_gen
Sourceval sexp_of_cofixpoint_expr : cofixpoint_expr -> Sexplib0.Sexp.t
Sourceval cofixpoint_expr_of_sexp : Sexplib0.Sexp.t -> cofixpoint_expr
Sourceval cofixpoint_expr_to_yojson : cofixpoint_expr -> Yojson.Safe.t
Sourceval hash_fold_cofixpoint_expr : Ppx_hash_lib.Std.Hash.state -> cofixpoint_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_cofixpoint_expr : cofixpoint_expr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_cofixpoint_expr : cofixpoint_expr -> cofixpoint_expr -> int
Sourcetype local_decl_expr = Vernacexpr.local_decl_expr =
  1. | AssumExpr of Names.lname * Constrexpr.local_binder_expr list * Constrexpr.constr_expr
  2. | DefExpr of Names.lname * Constrexpr.local_binder_expr list * Constrexpr.constr_expr * Constrexpr.constr_expr option
Sourceval sexp_of_local_decl_expr : local_decl_expr -> Sexplib0.Sexp.t
Sourceval local_decl_expr_of_sexp : Sexplib0.Sexp.t -> local_decl_expr
Sourceval local_decl_expr_to_yojson : local_decl_expr -> Yojson.Safe.t
Sourceval hash_fold_local_decl_expr : Ppx_hash_lib.Std.Hash.state -> local_decl_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_local_decl_expr : local_decl_expr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_local_decl_expr : local_decl_expr -> local_decl_expr -> int
Sourcetype inductive_kind = Vernacexpr.inductive_kind =
  1. | Inductive_kw
  2. | CoInductive
  3. | Variant
  4. | Record
  5. | Structure
  6. | Class of bool
Sourceval sexp_of_inductive_kind : inductive_kind -> Sexplib0.Sexp.t
Sourceval inductive_kind_of_sexp : Sexplib0.Sexp.t -> inductive_kind
Sourceval inductive_kind_to_yojson : inductive_kind -> Yojson.Safe.t
Sourceval hash_fold_inductive_kind : Ppx_hash_lib.Std.Hash.state -> inductive_kind -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_inductive_kind : inductive_kind -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_inductive_kind : inductive_kind -> inductive_kind -> int
Sourcetype simple_binder = Names.lident list * Constrexpr.constr_expr
Sourceval sexp_of_simple_binder : simple_binder -> Sexplib0.Sexp.t
Sourceval simple_binder_of_sexp : Sexplib0.Sexp.t -> simple_binder
Sourceval simple_binder_to_yojson : simple_binder -> Yojson.Safe.t
Sourceval hash_fold_simple_binder : Ppx_hash_lib.Std.Hash.state -> simple_binder -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_simple_binder : simple_binder -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_simple_binder : simple_binder -> simple_binder -> int
Sourcetype class_binder = Names.lident * Constrexpr.constr_expr list
Sourceval sexp_of_class_binder : class_binder -> Sexplib0.Sexp.t
Sourceval class_binder_of_sexp : Sexplib0.Sexp.t -> class_binder
Sourceval class_binder_to_yojson : class_binder -> Yojson.Safe.t
Sourceval hash_fold_class_binder : Ppx_hash_lib.Std.Hash.state -> class_binder -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_class_binder : class_binder -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_class_binder : class_binder -> class_binder -> int
Sourcetype 'a with_coercion = coercion_flag * 'a
Sourceval sexp_of_with_coercion : ('a -> Sexplib0.Sexp.t) -> 'a with_coercion -> Sexplib0.Sexp.t
Sourceval with_coercion_of_sexp : (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a with_coercion
Sourceval with_coercion_to_yojson : ('a -> Yojson.Safe.t) -> 'a with_coercion -> Yojson.Safe.t
Sourceval hash_fold_with_coercion : (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'a with_coercion -> Ppx_hash_lib.Std.Hash.state
Sourceval compare_with_coercion : ('a -> 'a -> int) -> 'a with_coercion -> 'a with_coercion -> int
Sourcetype 'a with_coercion_instance = (Attributes.vernac_flags * coercion_flag * instance_flag) * 'a
Sourceval sexp_of_with_coercion_instance : ('a -> Sexplib0.Sexp.t) -> 'a with_coercion_instance -> Sexplib0.Sexp.t
Sourceval with_coercion_instance_of_sexp : (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a with_coercion_instance
Sourceval with_coercion_instance_to_yojson : ('a -> Yojson.Safe.t) -> 'a with_coercion_instance -> Yojson.Safe.t
Sourceval hash_fold_with_coercion_instance : (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'a with_coercion_instance -> Ppx_hash_lib.Std.Hash.state
Sourceval compare_with_coercion_instance : ('a -> 'a -> int) -> 'a with_coercion_instance -> 'a with_coercion_instance -> int
Sourcetype constructor_expr = (Names.lident * Constrexpr.constr_expr) with_coercion_instance
Sourceval sexp_of_constructor_expr : constructor_expr -> Sexplib0.Sexp.t
Sourceval constructor_expr_of_sexp : Sexplib0.Sexp.t -> constructor_expr
Sourceval constructor_expr_to_yojson : constructor_expr -> Yojson.Safe.t
Sourceval hash_fold_constructor_expr : Ppx_hash_lib.Std.Hash.state -> constructor_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_constructor_expr : constructor_expr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_constructor_expr : constructor_expr -> constructor_expr -> int
Sourcetype 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;
}
Sourceval sexp_of_record_field_attr_unparsed : record_field_attr_unparsed -> Sexplib0.Sexp.t
Sourceval record_field_attr_unparsed_of_sexp : Sexplib0.Sexp.t -> record_field_attr_unparsed
Sourceval record_field_attr_unparsed_to_yojson : record_field_attr_unparsed -> Yojson.Safe.t
Sourceval hash_fold_record_field_attr_unparsed : Ppx_hash_lib.Std.Hash.state -> record_field_attr_unparsed -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_record_field_attr_unparsed : record_field_attr_unparsed -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_record_field_attr_unparsed : record_field_attr_unparsed -> record_field_attr_unparsed -> int
Sourcetype 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
Sourceval sexp_of_constructor_list_or_record_decl_expr : constructor_list_or_record_decl_expr -> Sexplib0.Sexp.t
Sourceval constructor_list_or_record_decl_expr_of_sexp : Sexplib0.Sexp.t -> constructor_list_or_record_decl_expr
Sourceval constructor_list_or_record_decl_expr_to_yojson : constructor_list_or_record_decl_expr -> Yojson.Safe.t
Sourceval hash_fold_constructor_list_or_record_decl_expr : Ppx_hash_lib.Std.Hash.state -> constructor_list_or_record_decl_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_constructor_list_or_record_decl_expr : constructor_list_or_record_decl_expr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_constructor_list_or_record_decl_expr : constructor_list_or_record_decl_expr -> constructor_list_or_record_decl_expr -> int
Sourcetype inductive_params_expr = Constrexpr.local_binder_expr list * Constrexpr.local_binder_expr list option
Sourceval sexp_of_inductive_params_expr : inductive_params_expr -> Sexplib0.Sexp.t
Sourceval inductive_params_expr_of_sexp : Sexplib0.Sexp.t -> inductive_params_expr
Sourceval inductive_params_expr_to_yojson : inductive_params_expr -> Yojson.Safe.t
Sourceval hash_fold_inductive_params_expr : Ppx_hash_lib.Std.Hash.state -> inductive_params_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_inductive_params_expr : inductive_params_expr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_inductive_params_expr : inductive_params_expr -> inductive_params_expr -> int
Sourcetype inductive_expr = Constrexpr.cumul_ident_decl with_coercion * inductive_params_expr * Constrexpr.constr_expr option * constructor_list_or_record_decl_expr
Sourceval sexp_of_inductive_expr : inductive_expr -> Sexplib0.Sexp.t
Sourceval inductive_expr_of_sexp : Sexplib0.Sexp.t -> inductive_expr
Sourceval inductive_expr_to_yojson : inductive_expr -> Yojson.Safe.t
Sourceval hash_fold_inductive_expr : Ppx_hash_lib.Std.Hash.state -> inductive_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_inductive_expr : inductive_expr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_inductive_expr : inductive_expr -> inductive_expr -> int
Sourcetype one_inductive_expr = Names.lident * inductive_params_expr * Constrexpr.constr_expr option * constructor_expr list
Sourceval sexp_of_one_inductive_expr : one_inductive_expr -> Sexplib0.Sexp.t
Sourceval one_inductive_expr_of_sexp : Sexplib0.Sexp.t -> one_inductive_expr
Sourceval one_inductive_expr_to_yojson : one_inductive_expr -> Yojson.Safe.t
Sourceval hash_fold_one_inductive_expr : Ppx_hash_lib.Std.Hash.state -> one_inductive_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_one_inductive_expr : one_inductive_expr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_one_inductive_expr : one_inductive_expr -> one_inductive_expr -> int
Sourcetype proof_expr = Constrexpr.ident_decl * (Constrexpr.local_binder_expr list * Constrexpr.constr_expr)
Sourceval sexp_of_proof_expr : proof_expr -> Sexplib0.Sexp.t
Sourceval proof_expr_of_sexp : Sexplib0.Sexp.t -> proof_expr
Sourceval proof_expr_to_yojson : proof_expr -> Yojson.Safe.t
Sourceval hash_fold_proof_expr : Ppx_hash_lib.Std.Hash.state -> proof_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_proof_expr : proof_expr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_proof_expr : proof_expr -> proof_expr -> int
Sourcetype proof_end = Vernacexpr.proof_end =
  1. | Admitted
  2. | Proved of opacity_flag * Names.lident option
Sourceval sexp_of_proof_end : proof_end -> Sexplib0.Sexp.t
Sourceval proof_end_of_sexp : Sexplib0.Sexp.t -> proof_end
Sourceval proof_end_to_yojson : proof_end -> Yojson.Safe.t
Sourceval hash_fold_proof_end : Ppx_hash_lib.Std.Hash.state -> proof_end -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_proof_end : proof_end -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_proof_end : proof_end -> proof_end -> int
Sourcetype scheme_type = Vernacexpr.scheme_type =
  1. | SchemeInduction
  2. | SchemeMinimality
  3. | SchemeElimination
  4. | SchemeCase
Sourceval sexp_of_scheme_type : scheme_type -> Sexplib0.Sexp.t
Sourceval scheme_type_of_sexp : Sexplib0.Sexp.t -> scheme_type
Sourceval scheme_type_to_yojson : scheme_type -> Yojson.Safe.t
Sourceval hash_fold_scheme_type : Ppx_hash_lib.Std.Hash.state -> scheme_type -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_scheme_type : scheme_type -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_scheme_type : scheme_type -> scheme_type -> int
Sourcetype scheme = Vernacexpr.scheme = {
  1. sch_type : scheme_type;
  2. sch_qualid : Libnames.qualid Constrexpr.or_by_notation;
  3. sch_sort : Sorts.family;
}
Sourceval sexp_of_scheme : scheme -> Sexplib0.Sexp.t
Sourceval scheme_of_sexp : Sexplib0.Sexp.t -> scheme
Sourceval scheme_to_yojson : scheme -> Yojson.Safe.t
Sourceval hash_fold_scheme : Ppx_hash_lib.Std.Hash.state -> scheme -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_scheme : scheme -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_scheme : scheme -> scheme -> int
Sourcetype 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
Sourceval sexp_of_section_subset_expr : section_subset_expr -> Sexplib0.Sexp.t
Sourceval section_subset_expr_of_sexp : Sexplib0.Sexp.t -> section_subset_expr
Sourceval section_subset_expr_to_yojson : section_subset_expr -> Yojson.Safe.t
Sourceval hash_fold_section_subset_expr : Ppx_hash_lib.Std.Hash.state -> section_subset_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_section_subset_expr : section_subset_expr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_section_subset_expr : section_subset_expr -> section_subset_expr -> int
Sourcetype extend_name = Vernacexpr.extend_name = {
  1. ext_plugin : string;
  2. ext_entry : string;
  3. ext_index : int;
}
Sourceval sexp_of_extend_name : extend_name -> Sexplib0.Sexp.t
Sourceval extend_name_of_sexp : Sexplib0.Sexp.t -> extend_name
Sourceval extend_name_to_yojson : extend_name -> Yojson.Safe.t
Sourceval hash_fold_extend_name : Ppx_hash_lib.Std.Hash.state -> extend_name -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_extend_name : extend_name -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_extend_name : extend_name -> extend_name -> int
Sourcetype register_kind = Vernacexpr.register_kind =
  1. | RegisterInline
  2. | RegisterCoqlib of Libnames.qualid
Sourceval sexp_of_register_kind : register_kind -> Sexplib0.Sexp.t
Sourceval register_kind_of_sexp : Sexplib0.Sexp.t -> register_kind
Sourceval register_kind_to_yojson : register_kind -> Yojson.Safe.t
Sourceval hash_fold_register_kind : Ppx_hash_lib.Std.Hash.state -> register_kind -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_register_kind : register_kind -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_register_kind : register_kind -> register_kind -> int
Sourcetype module_ast_inl = Constrexpr.module_ast * Declaremods.inline
Sourceval sexp_of_module_ast_inl : module_ast_inl -> Sexplib0.Sexp.t
Sourceval module_ast_inl_of_sexp : Sexplib0.Sexp.t -> module_ast_inl
Sourceval module_ast_inl_to_yojson : module_ast_inl -> Yojson.Safe.t
Sourceval hash_fold_module_ast_inl : Ppx_hash_lib.Std.Hash.state -> module_ast_inl -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_module_ast_inl : module_ast_inl -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_module_ast_inl : module_ast_inl -> module_ast_inl -> int
Sourcetype discharge = Vernacexpr.discharge =
  1. | DoDischarge
  2. | NoDischarge
Sourceval sexp_of_discharge : discharge -> Sexplib0.Sexp.t
Sourceval discharge_of_sexp : Sexplib0.Sexp.t -> discharge
Sourceval discharge_to_yojson : discharge -> Yojson.Safe.t
Sourceval hash_fold_discharge : Ppx_hash_lib.Std.Hash.state -> discharge -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_discharge : discharge -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_discharge : discharge -> discharge -> int
Sourcetype equality_scheme_type = Vernacexpr.equality_scheme_type =
  1. | SchemeBooleanEquality
  2. | SchemeEquality
Sourceval sexp_of_equality_scheme_type : equality_scheme_type -> Sexplib0.Sexp.t
Sourceval equality_scheme_type_of_sexp : Sexplib0.Sexp.t -> equality_scheme_type
Sourceval equality_scheme_type_to_yojson : equality_scheme_type -> Yojson.Safe.t
Sourceval hash_fold_equality_scheme_type : Ppx_hash_lib.Std.Hash.state -> equality_scheme_type -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_equality_scheme_type : equality_scheme_type -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_equality_scheme_type : equality_scheme_type -> equality_scheme_type -> int
Sourcetype import_categories = Vernacexpr.import_categories = {
  1. negative : bool;
  2. import_cats : string CAst.t list;
}
Sourceval sexp_of_import_categories : import_categories -> Sexplib0.Sexp.t
Sourceval import_categories_of_sexp : Sexplib0.Sexp.t -> import_categories
Sourceval import_categories_to_yojson : import_categories -> Yojson.Safe.t
Sourceval hash_fold_import_categories : Ppx_hash_lib.Std.Hash.state -> import_categories -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_import_categories : import_categories -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_import_categories : import_categories -> import_categories -> int
Sourcetype export_with_cats = export_flag * import_categories option
Sourceval sexp_of_export_with_cats : export_with_cats -> Sexplib0.Sexp.t
Sourceval export_with_cats_of_sexp : Sexplib0.Sexp.t -> export_with_cats
Sourceval export_with_cats_to_yojson : export_with_cats -> Yojson.Safe.t
Sourceval hash_fold_export_with_cats : Ppx_hash_lib.Std.Hash.state -> export_with_cats -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_export_with_cats : export_with_cats -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_export_with_cats : export_with_cats -> export_with_cats -> int
Sourcetype module_binder = export_with_cats option * Names.lident list * module_ast_inl
Sourceval sexp_of_module_binder : module_binder -> Sexplib0.Sexp.t
Sourceval module_binder_of_sexp : Sexplib0.Sexp.t -> module_binder
Sourceval module_binder_to_yojson : module_binder -> Yojson.Safe.t
Sourceval hash_fold_module_binder : Ppx_hash_lib.Std.Hash.state -> module_binder -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_module_binder : module_binder -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_module_binder : module_binder -> module_binder -> int
Sourcetype one_import_filter_name = Libnames.qualid * bool
Sourceval sexp_of_one_import_filter_name : one_import_filter_name -> Sexplib0.Sexp.t
Sourceval one_import_filter_name_of_sexp : Sexplib0.Sexp.t -> one_import_filter_name
Sourceval one_import_filter_name_to_yojson : one_import_filter_name -> Yojson.Safe.t
Sourceval hash_fold_one_import_filter_name : Ppx_hash_lib.Std.Hash.state -> one_import_filter_name -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_one_import_filter_name : one_import_filter_name -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_one_import_filter_name : one_import_filter_name -> one_import_filter_name -> int
Sourcetype import_filter_expr = Vernacexpr.import_filter_expr =
  1. | ImportAll
  2. | ImportNames of one_import_filter_name list
Sourceval sexp_of_import_filter_expr : import_filter_expr -> Sexplib0.Sexp.t
Sourceval import_filter_expr_of_sexp : Sexplib0.Sexp.t -> import_filter_expr
Sourceval import_filter_expr_to_yojson : import_filter_expr -> Yojson.Safe.t
Sourceval hash_fold_import_filter_expr : Ppx_hash_lib.Std.Hash.state -> import_filter_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_import_filter_expr : import_filter_expr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_import_filter_expr : import_filter_expr -> import_filter_expr -> int
Sourcetype hint_info_expr = Constrexpr.constr_pattern_expr Typeclasses.hint_info_gen
Sourceval sexp_of_hint_info_expr : hint_info_expr -> Sexplib0.Sexp.t
Sourceval hint_info_expr_of_sexp : Sexplib0.Sexp.t -> hint_info_expr
Sourceval hint_info_expr_to_yojson : hint_info_expr -> Yojson.Safe.t
Sourceval hash_fold_hint_info_expr : Ppx_hash_lib.Std.Hash.state -> hint_info_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_hint_info_expr : hint_info_expr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_hint_info_expr : hint_info_expr -> hint_info_expr -> int
Sourcetype reference_or_constr = Vernacexpr.reference_or_constr =
  1. | HintsReference of Libnames.qualid
  2. | HintsConstr of Constrexpr.constr_expr
Sourceval sexp_of_reference_or_constr : reference_or_constr -> Sexplib0.Sexp.t
Sourceval reference_or_constr_of_sexp : Sexplib0.Sexp.t -> reference_or_constr
Sourceval reference_or_constr_to_yojson : reference_or_constr -> Yojson.Safe.t
Sourceval hash_fold_reference_or_constr : Ppx_hash_lib.Std.Hash.state -> reference_or_constr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_reference_or_constr : reference_or_constr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_reference_or_constr : reference_or_constr -> reference_or_constr -> int
Sourcetype 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
Sourceval sexp_of_hints_expr : hints_expr -> Sexplib0.Sexp.t
Sourceval hints_expr_of_sexp : Sexplib0.Sexp.t -> hints_expr
Sourceval hints_expr_to_yojson : hints_expr -> Yojson.Safe.t
Sourceval hash_fold_hints_expr : Ppx_hash_lib.Std.Hash.state -> hints_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_hints_expr : hints_expr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_hints_expr : hints_expr -> hints_expr -> int
Sourcetype 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;
}
Sourceval sexp_of_vernac_one_argument_status : vernac_one_argument_status -> Sexplib0.Sexp.t
Sourceval vernac_one_argument_status_of_sexp : Sexplib0.Sexp.t -> vernac_one_argument_status
Sourceval vernac_one_argument_status_to_yojson : vernac_one_argument_status -> Yojson.Safe.t
Sourceval hash_fold_vernac_one_argument_status : Ppx_hash_lib.Std.Hash.state -> vernac_one_argument_status -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_vernac_one_argument_status : vernac_one_argument_status -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_vernac_one_argument_status : vernac_one_argument_status -> vernac_one_argument_status -> int
Sourcetype vernac_argument_status = Vernacexpr.vernac_argument_status =
  1. | VolatileArg
  2. | BidiArg
  3. | RealArg of vernac_one_argument_status
Sourceval sexp_of_vernac_argument_status : vernac_argument_status -> Sexplib0.Sexp.t
Sourceval vernac_argument_status_of_sexp : Sexplib0.Sexp.t -> vernac_argument_status
Sourceval vernac_argument_status_to_yojson : vernac_argument_status -> Yojson.Safe.t
Sourceval hash_fold_vernac_argument_status : Ppx_hash_lib.Std.Hash.state -> vernac_argument_status -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_vernac_argument_status : vernac_argument_status -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_vernac_argument_status : vernac_argument_status -> vernac_argument_status -> int
Sourcetype arguments_modifier = [
  1. | `DefaultImplicits
  2. | `ClearScopes
  3. | `ReductionNeverUnfold
  4. | `ExtraScopes
  5. | `ClearImplicits
  6. | `ClearBidiHint
  7. | `Assert
  8. | `Rename
  9. | `ReductionDontExposeCase
]
Sourceval sexp_of_arguments_modifier : arguments_modifier -> Sexplib0.Sexp.t
Sourceval arguments_modifier_of_sexp : Sexplib0.Sexp.t -> arguments_modifier
Sourceval __arguments_modifier_of_sexp__ : Sexplib0.Sexp.t -> arguments_modifier
Sourceval arguments_modifier_to_yojson : arguments_modifier -> Yojson.Safe.t
Sourceval hash_fold_arguments_modifier : Ppx_hash_lib.Std.Hash.state -> arguments_modifier -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_arguments_modifier : arguments_modifier -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_arguments_modifier : arguments_modifier -> arguments_modifier -> int
Sourcetype option_setting = Vernacexpr.option_setting =
  1. | OptionUnset
  2. | OptionSetTrue
  3. | OptionSetInt of int
  4. | OptionSetString of string
Sourceval sexp_of_option_setting : option_setting -> Sexplib0.Sexp.t
Sourceval option_setting_of_sexp : Sexplib0.Sexp.t -> option_setting
Sourceval option_setting_to_yojson : option_setting -> Yojson.Safe.t
Sourceval hash_fold_option_setting : Ppx_hash_lib.Std.Hash.state -> option_setting -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_option_setting : option_setting -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_option_setting : option_setting -> option_setting -> int
Sourcetype notation_enable_modifier = Vernacexpr.notation_enable_modifier =
  1. | EnableNotationEntry of Constrexpr.notation_entry CAst.t
  2. | EnableNotationOnly of Notationextern.notation_use
  3. | EnableNotationAll
Sourceval sexp_of_notation_enable_modifier : notation_enable_modifier -> Sexplib0.Sexp.t
Sourceval notation_enable_modifier_of_sexp : Sexplib0.Sexp.t -> notation_enable_modifier
Sourceval notation_enable_modifier_to_yojson : notation_enable_modifier -> Yojson.Safe.t
Sourceval hash_fold_notation_enable_modifier : Ppx_hash_lib.Std.Hash.state -> notation_enable_modifier -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_notation_enable_modifier : notation_enable_modifier -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_notation_enable_modifier : notation_enable_modifier -> notation_enable_modifier -> int
Sourcetype 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
Sourceval sexp_of_synterp_vernac_expr : synterp_vernac_expr -> Sexplib0.Sexp.t
Sourceval synterp_vernac_expr_of_sexp : Sexplib0.Sexp.t -> synterp_vernac_expr
Sourceval synterp_vernac_expr_to_yojson : synterp_vernac_expr -> Yojson.Safe.t
Sourceval hash_fold_synterp_vernac_expr : Ppx_hash_lib.Std.Hash.state -> synterp_vernac_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_synterp_vernac_expr : synterp_vernac_expr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_synterp_vernac_expr : synterp_vernac_expr -> synterp_vernac_expr -> int
Sourcetype 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
Sourceval sexp_of_synpure_vernac_expr : synpure_vernac_expr -> Sexplib0.Sexp.t
Sourceval synpure_vernac_expr_of_sexp : Sexplib0.Sexp.t -> synpure_vernac_expr
Sourceval synpure_vernac_expr_to_yojson : synpure_vernac_expr -> Yojson.Safe.t
Sourceval hash_fold_synpure_vernac_expr : Ppx_hash_lib.Std.Hash.state -> synpure_vernac_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_synpure_vernac_expr : synpure_vernac_expr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_synpure_vernac_expr : synpure_vernac_expr -> synpure_vernac_expr -> int
Sourcetype 'a vernac_expr_gen = 'a Vernacexpr.vernac_expr_gen =
  1. | VernacSynterp of 'a
  2. | VernacSynPure of synpure_vernac_expr
Sourceval sexp_of_vernac_expr_gen : ('a -> Sexplib0.Sexp.t) -> 'a vernac_expr_gen -> Sexplib0.Sexp.t
Sourceval vernac_expr_gen_of_sexp : (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a vernac_expr_gen
Sourceval vernac_expr_gen_to_yojson : ('a -> Yojson.Safe.t) -> 'a vernac_expr_gen -> Yojson.Safe.t
Sourceval hash_fold_vernac_expr_gen : (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'a vernac_expr_gen -> Ppx_hash_lib.Std.Hash.state
Sourceval compare_vernac_expr_gen : ('a -> 'a -> int) -> 'a vernac_expr_gen -> 'a vernac_expr_gen -> int
Sourcetype control_flag = Vernacexpr.control_flag =
  1. | ControlTime
  2. | ControlInstructions
  3. | ControlRedirect of string
  4. | ControlTimeout of int
  5. | ControlFail
  6. | ControlSucceed
Sourceval sexp_of_control_flag : control_flag -> Sexplib0.Sexp.t
Sourceval control_flag_of_sexp : Sexplib0.Sexp.t -> control_flag
Sourceval control_flag_to_yojson : control_flag -> Yojson.Safe.t
Sourceval hash_fold_control_flag : Ppx_hash_lib.Std.Hash.state -> control_flag -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_control_flag : control_flag -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_control_flag : control_flag -> control_flag -> int
Sourcetype ('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;
}
Sourceval sexp_of_vernac_control_gen_r : ('a -> Sexplib0.Sexp.t) -> ('b -> Sexplib0.Sexp.t) -> ('a, 'b) vernac_control_gen_r -> Sexplib0.Sexp.t
Sourceval vernac_control_gen_r_of_sexp : (Sexplib0.Sexp.t -> 'a) -> (Sexplib0.Sexp.t -> 'b) -> Sexplib0.Sexp.t -> ('a, 'b) vernac_control_gen_r
Sourceval vernac_control_gen_r_to_yojson : ('a -> Yojson.Safe.t) -> ('b -> Yojson.Safe.t) -> ('a, 'b) vernac_control_gen_r -> Yojson.Safe.t
Sourceval hash_fold_vernac_control_gen_r : (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) -> (Ppx_hash_lib.Std.Hash.state -> 'b -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> ('a, 'b) vernac_control_gen_r -> Ppx_hash_lib.Std.Hash.state
Sourceval compare_vernac_control_gen_r : ('a -> 'a -> int) -> ('b -> 'b -> int) -> ('a, 'b) vernac_control_gen_r -> ('a, 'b) vernac_control_gen_r -> int
Sourcetype 'a vernac_control_gen = (control_flag, 'a) vernac_control_gen_r CAst.t
Sourceval sexp_of_vernac_control_gen : ('a -> Sexplib0.Sexp.t) -> 'a vernac_control_gen -> Sexplib0.Sexp.t
Sourceval vernac_control_gen_of_sexp : (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a vernac_control_gen
Sourceval vernac_control_gen_to_yojson : ('a -> Yojson.Safe.t) -> 'a vernac_control_gen -> Yojson.Safe.t
Sourceval hash_fold_vernac_control_gen : (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'a vernac_control_gen -> Ppx_hash_lib.Std.Hash.state
Sourceval compare_vernac_control_gen : ('a -> 'a -> int) -> 'a vernac_control_gen -> 'a vernac_control_gen -> int
Sourceval sexp_of_vernac_control : vernac_control -> Sexplib0.Sexp.t
Sourceval vernac_control_of_sexp : Sexplib0.Sexp.t -> vernac_control
Sourceval vernac_control_to_yojson : vernac_control -> Yojson.Safe.t
Sourceval hash_fold_vernac_control : Ppx_hash_lib.Std.Hash.state -> vernac_control -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_vernac_control : vernac_control -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_vernac_control : vernac_control -> vernac_control -> int