Module `Serlib.Ser_vernacexpr`Source

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

val infix_flag_of_yojson : 
  Yojson.Safe.t ->
  infix_flag Ppx_deriving_yojson_runtime.error_or

Source

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

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

Source

val opacity_flag_of_yojson : 
  Yojson.Safe.t ->
  opacity_flag Ppx_deriving_yojson_runtime.error_or

Source

val 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

Source

val scope_name_of_yojson : 
  Yojson.Safe.t ->
  scope_name Ppx_deriving_yojson_runtime.error_or

Source

val 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 notation_format = Vernacexpr.notation_format =

| 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

Source

val notation_format_of_yojson : 
  Yojson.Safe.t ->
  notation_format Ppx_deriving_yojson_runtime.error_or

Source

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

| SetItemLevel of string list * Notation_term.notation_binder_kind option * Extend.production_level
| SetItemScope of string list * scope_name
| SetLevel of int
| SetCustomEntry of string * int option
| SetAssoc of Gramlib.Gramext.g_assoc
| SetEntryType of string * Extend.simple_constr_prod_entry_key
| SetOnlyParsing
| SetOnlyPrinting
| 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

Source

val syntax_modifier_of_yojson : 
  Yojson.Safe.t ->
  syntax_modifier Ppx_deriving_yojson_runtime.error_or

Source

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

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

Source

val coercion_class_of_yojson : 
  Yojson.Safe.t ->
  coercion_class Ppx_deriving_yojson_runtime.error_or

Source

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

| OpenSubgoals
| NthGoal of int
| 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

Source

val goal_reference_of_yojson : 
  Yojson.Safe.t ->
  goal_reference Ppx_deriving_yojson_runtime.error_or

Source

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

| PrintTypingFlags
| PrintTables
| PrintFullContext
| PrintSectionContext of Libnames.qualid
| PrintInspect of int
| PrintGrammar of string list
| PrintCustomGrammar of string
| PrintKeywords
| PrintLoadPath of Names.DirPath.t option
| PrintLibraries
| PrintModule of Libnames.qualid
| PrintModuleType of Libnames.qualid
| PrintNamespace of Names.DirPath.t
| PrintMLLoadPath
| PrintMLModules
| PrintDebugGC
| PrintName of Libnames.qualid Constrexpr.or_by_notation * UnivNames.univ_name_list option
| PrintGraph
| PrintClasses
| PrintTypeclasses
| PrintInstances of Libnames.qualid Constrexpr.or_by_notation
| PrintCoercions
| PrintCoercionPaths of coercion_class * coercion_class
| PrintCanonicalConversions of Libnames.qualid Constrexpr.or_by_notation list
| PrintUniverses of bool * Libnames.qualid list option * string option
| PrintHint of Libnames.qualid Constrexpr.or_by_notation
| PrintHintGoal
| PrintHintDbName of string
| PrintHintDb
| PrintScopes
| PrintScope of string
| PrintVisibility of string option
| PrintAbout of Libnames.qualid Constrexpr.or_by_notation * UnivNames.univ_name_list option * Goal_select.t option
| PrintImplicit of Libnames.qualid Constrexpr.or_by_notation
| PrintAssumptions of bool * bool * Libnames.qualid Constrexpr.or_by_notation
| PrintStrategy of Libnames.qualid Constrexpr.or_by_notation option
| PrintRegistered
| 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

Source

val printable_of_yojson : 
  Yojson.Safe.t ->
  printable Ppx_deriving_yojson_runtime.error_or

Source

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

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

Source

val glob_search_where_of_yojson : 
  Yojson.Safe.t ->
  glob_search_where Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_glob_search_where : 
  Ppx_hash_lib.Std.Hash.state ->
  glob_search_where ->
  Ppx_hash_lib.Std.Hash.state

Source

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

| SearchSubPattern of glob_search_where * bool * Constrexpr.constr_pattern_expr
| SearchString of glob_search_where * bool * string * scope_name option
| 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

Source

val search_item_of_yojson : 
  Yojson.Safe.t ->
  search_item Ppx_deriving_yojson_runtime.error_or

Source

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

| SearchLiteral of search_item
| 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

Source

val search_request_of_yojson : 
  Yojson.Safe.t ->
  search_request Ppx_deriving_yojson_runtime.error_or

Source

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

| SearchPattern of Constrexpr.constr_pattern_expr
| SearchRewrite of Constrexpr.constr_pattern_expr
| 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

Source

val searchable_of_yojson : 
  Yojson.Safe.t ->
  searchable Ppx_deriving_yojson_runtime.error_or

Source

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

| LocateAny of Libnames.qualid Constrexpr.or_by_notation
| LocateTerm of Libnames.qualid Constrexpr.or_by_notation
| LocateLibrary of Libnames.qualid
| LocateModule of Libnames.qualid
| LocateOther of string * Libnames.qualid
| 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

Source

val locatable_of_yojson : 
  Yojson.Safe.t ->
  locatable Ppx_deriving_yojson_runtime.error_or

Source

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

| ShowGoal of goal_reference
| ShowProof
| ShowExistentials
| ShowUniverses
| ShowProofNames
| ShowIntros of bool
| 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

Source

val showable_of_yojson : 
  Yojson.Safe.t ->
  showable Ppx_deriving_yojson_runtime.error_or

Source

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

| CommentConstr of Constrexpr.constr_expr
| CommentString of string
| 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

Source

val comment_of_yojson : 
  Yojson.Safe.t ->
  comment Ppx_deriving_yojson_runtime.error_or

Source

val 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 search_restriction = Vernacexpr.search_restriction =

| SearchInside of Libnames.qualid list
| SearchOutside of Libnames.qualid list

Sourceval sexp_of_search_restriction : search_restriction -> Sexplib0.Sexp.t

Sourceval search_restriction_of_sexp : Sexplib0.Sexp.t -> search_restriction

Sourceval search_restriction_to_yojson : search_restriction -> Yojson.Safe.t

Source

val search_restriction_of_yojson : 
  Yojson.Safe.t ->
  search_restriction Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_search_restriction : 
  Ppx_hash_lib.Std.Hash.state ->
  search_restriction ->
  Ppx_hash_lib.Std.Hash.state

Source

val hash_search_restriction : 
  search_restriction ->
  Ppx_hash_lib.Std.Hash.hash_value

Source

val compare_search_restriction : 
  search_restriction ->
  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

Source

val verbose_flag_of_yojson : 
  Yojson.Safe.t ->
  verbose_flag Ppx_deriving_yojson_runtime.error_or

Source

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

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

Source

val coercion_flag_of_yojson : 
  Yojson.Safe.t ->
  coercion_flag Ppx_deriving_yojson_runtime.error_or

Source

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

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

Source

val instance_flag_of_yojson : 
  Yojson.Safe.t ->
  instance_flag Ppx_deriving_yojson_runtime.error_or

Source

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

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

Source

val export_flag_of_yojson : 
  Yojson.Safe.t ->
  export_flag Ppx_deriving_yojson_runtime.error_or

Source

val 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

Source

val locality_flag_of_yojson : 
  Yojson.Safe.t ->
  locality_flag Ppx_deriving_yojson_runtime.error_or

Source

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

| ProveBody of Constrexpr.local_binder_expr list * Constrexpr.constr_expr
| 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

Source

val definition_expr_of_yojson : 
  Yojson.Safe.t ->
  definition_expr Ppx_deriving_yojson_runtime.error_or

Source

val 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 = {

ntn_decl_string : Names.lstring;
ntn_decl_interp : Constrexpr.constr_expr;
ntn_decl_scope : scope_name option;
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

Source

val notation_declaration_of_yojson : 
  Yojson.Safe.t ->
  notation_declaration Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_notation_declaration : 
  Ppx_hash_lib.Std.Hash.state ->
  notation_declaration ->
  Ppx_hash_lib.Std.Hash.state

Source

val hash_notation_declaration : 
  notation_declaration ->
  Ppx_hash_lib.Std.Hash.hash_value

Source

val compare_notation_declaration : 
  notation_declaration ->
  notation_declaration ->
  int

Sourcetype 'a fix_expr_gen = 'a Vernacexpr.fix_expr_gen = {

fname : Names.lident;
univs : Constrexpr.universe_decl_expr option;
rec_order : 'a;
binders : Constrexpr.local_binder_expr list;
rtype : Constrexpr.constr_expr;
body_def : Constrexpr.constr_expr option;
notations : notation_declaration list;

}

Source

val sexp_of_fix_expr_gen : 
  ('a -> Sexplib0.Sexp.t) ->
  'a fix_expr_gen ->
  Sexplib0.Sexp.t

Source

val fix_expr_gen_of_sexp : 
  (Sexplib0.Sexp.t -> 'a) ->
  Sexplib0.Sexp.t ->
  'a fix_expr_gen

Source

val fix_expr_gen_to_yojson : 
  ('a -> Yojson.Safe.t) ->
  'a fix_expr_gen ->
  Yojson.Safe.t

Source

val fix_expr_gen_of_yojson : 
  (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  'a fix_expr_gen Ppx_deriving_yojson_runtime.error_or

Source

val 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

Source

val 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

Source

val fixpoint_expr_of_yojson : 
  Yojson.Safe.t ->
  fixpoint_expr Ppx_deriving_yojson_runtime.error_or

Source

val 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

Source

val cofixpoint_expr_of_yojson : 
  Yojson.Safe.t ->
  cofixpoint_expr Ppx_deriving_yojson_runtime.error_or

Source

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

| AssumExpr of Names.lname * Constrexpr.local_binder_expr list * Constrexpr.constr_expr
| 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

Source

val local_decl_expr_of_yojson : 
  Yojson.Safe.t ->
  local_decl_expr Ppx_deriving_yojson_runtime.error_or

Source

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

| Inductive_kw
| CoInductive
| Variant
| Record
| Structure
| 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

Source

val inductive_kind_of_yojson : 
  Yojson.Safe.t ->
  inductive_kind Ppx_deriving_yojson_runtime.error_or

Source

val 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

Source

val simple_binder_of_yojson : 
  Yojson.Safe.t ->
  simple_binder Ppx_deriving_yojson_runtime.error_or

Source

val 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

Source

val class_binder_of_yojson : 
  Yojson.Safe.t ->
  class_binder Ppx_deriving_yojson_runtime.error_or

Source

val 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

Source

val sexp_of_with_coercion : 
  ('a -> Sexplib0.Sexp.t) ->
  'a with_coercion ->
  Sexplib0.Sexp.t

Source

val with_coercion_of_sexp : 
  (Sexplib0.Sexp.t -> 'a) ->
  Sexplib0.Sexp.t ->
  'a with_coercion

Source

val with_coercion_to_yojson : 
  ('a -> Yojson.Safe.t) ->
  'a with_coercion ->
  Yojson.Safe.t

Source

val with_coercion_of_yojson : 
  (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  'a with_coercion Ppx_deriving_yojson_runtime.error_or

Source

val 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

Source

val compare_with_coercion : 
  ('a -> 'a -> int) ->
  'a with_coercion ->
  'a with_coercion ->
  int

Source

type 'a with_coercion_instance =
  (Attributes.vernac_flags * coercion_flag * instance_flag) * 'a

Source

val sexp_of_with_coercion_instance : 
  ('a -> Sexplib0.Sexp.t) ->
  'a with_coercion_instance ->
  Sexplib0.Sexp.t

Source

val with_coercion_instance_of_sexp : 
  (Sexplib0.Sexp.t -> 'a) ->
  Sexplib0.Sexp.t ->
  'a with_coercion_instance

Source

val with_coercion_instance_to_yojson : 
  ('a -> Yojson.Safe.t) ->
  'a with_coercion_instance ->
  Yojson.Safe.t

Source

val with_coercion_instance_of_yojson : 
  (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  'a with_coercion_instance Ppx_deriving_yojson_runtime.error_or

Source

val 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

Source

val compare_with_coercion_instance : 
  ('a -> 'a -> int) ->
  'a with_coercion_instance ->
  'a with_coercion_instance ->
  int

Source

type 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

Source

val constructor_expr_of_yojson : 
  Yojson.Safe.t ->
  constructor_expr Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_constructor_expr : 
  Ppx_hash_lib.Std.Hash.state ->
  constructor_expr ->
  Ppx_hash_lib.Std.Hash.state

Source

val 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 = {

rfu_attrs : Attributes.vernac_flags;
rfu_coercion : coercion_flag;
rfu_instance : instance_flag;
rfu_priority : int option;
rfu_notation : notation_declaration list;

}

Source

val sexp_of_record_field_attr_unparsed : 
  record_field_attr_unparsed ->
  Sexplib0.Sexp.t

Source

val record_field_attr_unparsed_of_sexp : 
  Sexplib0.Sexp.t ->
  record_field_attr_unparsed

Source

val record_field_attr_unparsed_to_yojson : 
  record_field_attr_unparsed ->
  Yojson.Safe.t

Source

val record_field_attr_unparsed_of_yojson : 
  Yojson.Safe.t ->
  record_field_attr_unparsed Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_record_field_attr_unparsed : 
  Ppx_hash_lib.Std.Hash.state ->
  record_field_attr_unparsed ->
  Ppx_hash_lib.Std.Hash.state

Source

val hash_record_field_attr_unparsed : 
  record_field_attr_unparsed ->
  Ppx_hash_lib.Std.Hash.hash_value

Source

val compare_record_field_attr_unparsed : 
  record_field_attr_unparsed ->
  record_field_attr_unparsed ->
  int

Source

type constructor_list_or_record_decl_expr =
  Vernacexpr.constructor_list_or_record_decl_expr =

| Constructors of constructor_expr list
| RecordDecl of Names.lident option * (local_decl_expr * record_field_attr_unparsed) list * Names.lident option

Source

val sexp_of_constructor_list_or_record_decl_expr : 
  constructor_list_or_record_decl_expr ->
  Sexplib0.Sexp.t

Source

val constructor_list_or_record_decl_expr_of_sexp : 
  Sexplib0.Sexp.t ->
  constructor_list_or_record_decl_expr

Source

val constructor_list_or_record_decl_expr_to_yojson : 
  constructor_list_or_record_decl_expr ->
  Yojson.Safe.t

Source

val constructor_list_or_record_decl_expr_of_yojson : 
  Yojson.Safe.t ->
  constructor_list_or_record_decl_expr Ppx_deriving_yojson_runtime.error_or

Source

val 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

Source

val hash_constructor_list_or_record_decl_expr : 
  constructor_list_or_record_decl_expr ->
  Ppx_hash_lib.Std.Hash.hash_value

Source

val compare_constructor_list_or_record_decl_expr : 
  constructor_list_or_record_decl_expr ->
  constructor_list_or_record_decl_expr ->
  int

Source

type 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

Source

val inductive_params_expr_of_yojson : 
  Yojson.Safe.t ->
  inductive_params_expr Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_inductive_params_expr : 
  Ppx_hash_lib.Std.Hash.state ->
  inductive_params_expr ->
  Ppx_hash_lib.Std.Hash.state

Source

val hash_inductive_params_expr : 
  inductive_params_expr ->
  Ppx_hash_lib.Std.Hash.hash_value

Source

val compare_inductive_params_expr : 
  inductive_params_expr ->
  inductive_params_expr ->
  int

Source

type 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

Source

val inductive_expr_of_yojson : 
  Yojson.Safe.t ->
  inductive_expr Ppx_deriving_yojson_runtime.error_or

Source

val 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

Source

type 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

Source

val one_inductive_expr_of_yojson : 
  Yojson.Safe.t ->
  one_inductive_expr Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_one_inductive_expr : 
  Ppx_hash_lib.Std.Hash.state ->
  one_inductive_expr ->
  Ppx_hash_lib.Std.Hash.state

Source

val hash_one_inductive_expr : 
  one_inductive_expr ->
  Ppx_hash_lib.Std.Hash.hash_value

Source

val compare_one_inductive_expr : 
  one_inductive_expr ->
  one_inductive_expr ->
  int

Source

type 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

Source

val proof_expr_of_yojson : 
  Yojson.Safe.t ->
  proof_expr Ppx_deriving_yojson_runtime.error_or

Source

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

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

Source

val proof_end_of_yojson : 
  Yojson.Safe.t ->
  proof_end Ppx_deriving_yojson_runtime.error_or

Source

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

| SchemeInduction
| SchemeMinimality
| SchemeElimination
| 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

Source

val scheme_type_of_yojson : 
  Yojson.Safe.t ->
  scheme_type Ppx_deriving_yojson_runtime.error_or

Source

val 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 = {

sch_type : scheme_type;
sch_qualid : Libnames.qualid Constrexpr.or_by_notation;
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

Source

val scheme_of_yojson : 
  Yojson.Safe.t ->
  scheme Ppx_deriving_yojson_runtime.error_or

Source

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

| SsEmpty
| SsType
| SsSingl of Names.lident
| SsCompl of section_subset_expr
| SsUnion of section_subset_expr * section_subset_expr
| SsSubstr of section_subset_expr * section_subset_expr
| 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

Source

val section_subset_expr_of_yojson : 
  Yojson.Safe.t ->
  section_subset_expr Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_section_subset_expr : 
  Ppx_hash_lib.Std.Hash.state ->
  section_subset_expr ->
  Ppx_hash_lib.Std.Hash.state

Source

val hash_section_subset_expr : 
  section_subset_expr ->
  Ppx_hash_lib.Std.Hash.hash_value

Source

val compare_section_subset_expr : 
  section_subset_expr ->
  section_subset_expr ->
  int

Sourcetype extend_name = string * 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

Source

val extend_name_of_yojson : 
  Yojson.Safe.t ->
  extend_name Ppx_deriving_yojson_runtime.error_or

Source

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

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

Source

val register_kind_of_yojson : 
  Yojson.Safe.t ->
  register_kind Ppx_deriving_yojson_runtime.error_or

Source

val 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

Source

val module_ast_inl_of_yojson : 
  Yojson.Safe.t ->
  module_ast_inl Ppx_deriving_yojson_runtime.error_or

Source

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

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

Source

val discharge_of_yojson : 
  Yojson.Safe.t ->
  discharge Ppx_deriving_yojson_runtime.error_or

Source

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

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

Source

val equality_scheme_type_of_yojson : 
  Yojson.Safe.t ->
  equality_scheme_type Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_equality_scheme_type : 
  Ppx_hash_lib.Std.Hash.state ->
  equality_scheme_type ->
  Ppx_hash_lib.Std.Hash.state

Source

val hash_equality_scheme_type : 
  equality_scheme_type ->
  Ppx_hash_lib.Std.Hash.hash_value

Source

val compare_equality_scheme_type : 
  equality_scheme_type ->
  equality_scheme_type ->
  int

Sourcetype import_categories = Vernacexpr.import_categories = {

negative : bool;
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

Source

val import_categories_of_yojson : 
  Yojson.Safe.t ->
  import_categories Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_import_categories : 
  Ppx_hash_lib.Std.Hash.state ->
  import_categories ->
  Ppx_hash_lib.Std.Hash.state

Source

val 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

Source

val export_with_cats_of_yojson : 
  Yojson.Safe.t ->
  export_with_cats Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_export_with_cats : 
  Ppx_hash_lib.Std.Hash.state ->
  export_with_cats ->
  Ppx_hash_lib.Std.Hash.state

Source

val 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

Source

type 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

Source

val module_binder_of_yojson : 
  Yojson.Safe.t ->
  module_binder Ppx_deriving_yojson_runtime.error_or

Source

val 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

Source

val one_import_filter_name_of_yojson : 
  Yojson.Safe.t ->
  one_import_filter_name Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_one_import_filter_name : 
  Ppx_hash_lib.Std.Hash.state ->
  one_import_filter_name ->
  Ppx_hash_lib.Std.Hash.state

Source

val hash_one_import_filter_name : 
  one_import_filter_name ->
  Ppx_hash_lib.Std.Hash.hash_value

Source

val compare_one_import_filter_name : 
  one_import_filter_name ->
  one_import_filter_name ->
  int

Sourcetype import_filter_expr = Vernacexpr.import_filter_expr =

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

Source

val import_filter_expr_of_yojson : 
  Yojson.Safe.t ->
  import_filter_expr Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_import_filter_expr : 
  Ppx_hash_lib.Std.Hash.state ->
  import_filter_expr ->
  Ppx_hash_lib.Std.Hash.state

Source

val hash_import_filter_expr : 
  import_filter_expr ->
  Ppx_hash_lib.Std.Hash.hash_value

Source

val 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

Source

val hint_info_expr_of_yojson : 
  Yojson.Safe.t ->
  hint_info_expr Ppx_deriving_yojson_runtime.error_or

Source

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

| HintsReference of Libnames.qualid
| 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

Source

val reference_or_constr_of_yojson : 
  Yojson.Safe.t ->
  reference_or_constr Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_reference_or_constr : 
  Ppx_hash_lib.Std.Hash.state ->
  reference_or_constr ->
  Ppx_hash_lib.Std.Hash.state

Source

val hash_reference_or_constr : 
  reference_or_constr ->
  Ppx_hash_lib.Std.Hash.hash_value

Source

val compare_reference_or_constr : 
  reference_or_constr ->
  reference_or_constr ->
  int

Sourcetype hints_expr = Vernacexpr.hints_expr =

| HintsResolve of (hint_info_expr * bool * reference_or_constr) list
| HintsResolveIFF of bool * Libnames.qualid list * int option
| HintsImmediate of reference_or_constr list
| HintsUnfold of Libnames.qualid list
| HintsTransparency of Libnames.qualid Hints.hints_transparency_target * bool
| HintsMode of Libnames.qualid * Hints.hint_mode list
| HintsConstructors of Libnames.qualid list
| 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

Source

val hints_expr_of_yojson : 
  Yojson.Safe.t ->
  hints_expr Ppx_deriving_yojson_runtime.error_or

Source

val 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 = {

name : Names.Name.t;
recarg_like : bool;
notation_scope : string CAst.t list;
implicit_status : Glob_term.binding_kind;

}

Source

val sexp_of_vernac_one_argument_status : 
  vernac_one_argument_status ->
  Sexplib0.Sexp.t

Source

val vernac_one_argument_status_of_sexp : 
  Sexplib0.Sexp.t ->
  vernac_one_argument_status

Source

val vernac_one_argument_status_to_yojson : 
  vernac_one_argument_status ->
  Yojson.Safe.t

Source

val vernac_one_argument_status_of_yojson : 
  Yojson.Safe.t ->
  vernac_one_argument_status Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_vernac_one_argument_status : 
  Ppx_hash_lib.Std.Hash.state ->
  vernac_one_argument_status ->
  Ppx_hash_lib.Std.Hash.state

Source

val hash_vernac_one_argument_status : 
  vernac_one_argument_status ->
  Ppx_hash_lib.Std.Hash.hash_value

Source

val compare_vernac_one_argument_status : 
  vernac_one_argument_status ->
  vernac_one_argument_status ->
  int

Sourcetype vernac_argument_status = Vernacexpr.vernac_argument_status =

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

Source

val vernac_argument_status_of_yojson : 
  Yojson.Safe.t ->
  vernac_argument_status Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_vernac_argument_status : 
  Ppx_hash_lib.Std.Hash.state ->
  vernac_argument_status ->
  Ppx_hash_lib.Std.Hash.state

Source

val hash_vernac_argument_status : 
  vernac_argument_status ->
  Ppx_hash_lib.Std.Hash.hash_value

Source

val compare_vernac_argument_status : 
  vernac_argument_status ->
  vernac_argument_status ->
  int

Sourcetype arguments_modifier = [

| `DefaultImplicits
| `ClearScopes
| `ReductionNeverUnfold
| `ExtraScopes
| `ClearImplicits
| `ClearBidiHint
| `Assert
| `Rename
| `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

Source

val arguments_modifier_of_yojson : 
  Yojson.Safe.t ->
  arguments_modifier Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_arguments_modifier : 
  Ppx_hash_lib.Std.Hash.state ->
  arguments_modifier ->
  Ppx_hash_lib.Std.Hash.state

Source

val hash_arguments_modifier : 
  arguments_modifier ->
  Ppx_hash_lib.Std.Hash.hash_value

Source

val compare_arguments_modifier : 
  arguments_modifier ->
  arguments_modifier ->
  int

Sourcetype option_setting = Vernacexpr.option_setting =

| OptionUnset
| OptionSetTrue
| OptionSetInt of int
| 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

Source

val option_setting_of_yojson : 
  Yojson.Safe.t ->
  option_setting Ppx_deriving_yojson_runtime.error_or

Source

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

| EnableNotationEntry of Constrexpr.notation_entry CAst.t
| EnableNotationOnly of Notationextern.notation_use
| EnableNotationAll

Source

val sexp_of_notation_enable_modifier : 
  notation_enable_modifier ->
  Sexplib0.Sexp.t

Source

val notation_enable_modifier_of_sexp : 
  Sexplib0.Sexp.t ->
  notation_enable_modifier

Source

val notation_enable_modifier_to_yojson : 
  notation_enable_modifier ->
  Yojson.Safe.t

Source

val notation_enable_modifier_of_yojson : 
  Yojson.Safe.t ->
  notation_enable_modifier Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_notation_enable_modifier : 
  Ppx_hash_lib.Std.Hash.state ->
  notation_enable_modifier ->
  Ppx_hash_lib.Std.Hash.state

Source

val hash_notation_enable_modifier : 
  notation_enable_modifier ->
  Ppx_hash_lib.Std.Hash.hash_value

Source

val compare_notation_enable_modifier : 
  notation_enable_modifier ->
  notation_enable_modifier ->
  int

Sourcetype synterp_vernac_expr = Vernacexpr.synterp_vernac_expr =

| VernacLoad of verbose_flag * string
| VernacReservedNotation of infix_flag * Names.lstring * syntax_modifier CAst.t list
| VernacNotation of infix_flag * notation_declaration
| VernacDeclareCustomEntry of string
| VernacBeginSection of Names.lident
| VernacEndSegment of Names.lident
| VernacRequire of Libnames.qualid option * export_with_cats option * (Libnames.qualid * import_filter_expr) list
| VernacImport of export_with_cats * (Libnames.qualid * import_filter_expr) list
| VernacDeclareModule of export_with_cats option * Names.lident * module_binder list * module_ast_inl
| VernacDefineModule of export_with_cats option * Names.lident * module_binder list * module_ast_inl Declaremods.module_signature * module_ast_inl list
| VernacDeclareModuleType of Names.lident * module_binder list * module_ast_inl list * module_ast_inl list
| VernacInclude of module_ast_inl list
| VernacDeclareMLModule of string list
| VernacChdir of string option
| VernacExtraDependency of Libnames.qualid * string * Names.Id.t option
| VernacSetOption of bool * Goptions.option_name * option_setting
| VernacProofMode of string
| 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

Source

val synterp_vernac_expr_of_yojson : 
  Yojson.Safe.t ->
  synterp_vernac_expr Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_synterp_vernac_expr : 
  Ppx_hash_lib.Std.Hash.state ->
  synterp_vernac_expr ->
  Ppx_hash_lib.Std.Hash.state

Source

val hash_synterp_vernac_expr : 
  synterp_vernac_expr ->
  Ppx_hash_lib.Std.Hash.hash_value

Source

val compare_synterp_vernac_expr : 
  synterp_vernac_expr ->
  synterp_vernac_expr ->
  int

Sourcetype synpure_vernac_expr = Vernacexpr.synpure_vernac_expr =

| VernacOpenCloseScope of bool * scope_name
| VernacDeclareScope of scope_name
| VernacDelimiters of scope_name * string option
| VernacBindScope of scope_name * coercion_class list
| 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
| VernacDefinition of discharge * Decls.definition_object_kind * Constrexpr.name_decl * definition_expr
| VernacStartTheoremProof of Decls.theorem_kind * proof_expr list
| VernacEndProof of proof_end
| VernacExactProof of Constrexpr.constr_expr
| VernacAssumption of discharge * Decls.assumption_object_kind * Declaremods.inline * (Constrexpr.ident_decl list * Constrexpr.constr_expr) with_coercion list
| VernacInductive of inductive_kind * (inductive_expr * notation_declaration list) list
| VernacFixpoint of discharge * fixpoint_expr list
| VernacCoFixpoint of discharge * cofixpoint_expr list
| VernacScheme of (Names.lident option * scheme) list
| VernacSchemeEquality of equality_scheme_type * Libnames.qualid Constrexpr.or_by_notation
| VernacCombinedScheme of Names.lident * Names.lident list
| VernacUniverse of Names.lident list
| VernacConstraint of Constrexpr.univ_constraint_expr list
| VernacCanonical of Libnames.qualid Constrexpr.or_by_notation
| VernacCoercion of Libnames.qualid Constrexpr.or_by_notation * (coercion_class * coercion_class) option
| VernacIdentityCoercion of Names.lident * coercion_class * coercion_class
| VernacNameSectionHypSet of Names.lident * section_subset_expr
| VernacInstance of Constrexpr.name_decl * Constrexpr.local_binder_expr list * Constrexpr.constr_expr * (bool * Constrexpr.constr_expr) option * hint_info_expr
| VernacDeclareInstance of Constrexpr.ident_decl * Constrexpr.local_binder_expr list * Constrexpr.constr_expr * hint_info_expr
| VernacContext of Constrexpr.local_binder_expr list
| VernacExistingInstance of (Libnames.qualid * hint_info_expr) list
| VernacExistingClass of Libnames.qualid
| VernacResetName of Names.lident
| VernacResetInitial
| VernacBack of int
| VernacCreateHintDb of string * bool
| VernacRemoveHints of string list * Libnames.qualid list
| VernacHints of string list * hints_expr
| VernacSyntacticDefinition of Names.lident * Names.Id.t list * Constrexpr.constr_expr * syntax_modifier CAst.t list
| VernacArguments of Libnames.qualid Constrexpr.or_by_notation * vernac_argument_status list * (Names.Name.t * Glob_term.binding_kind) list list * arguments_modifier list
| VernacReserve of simple_binder list
| VernacGeneralizable of Names.lident list option
| VernacSetOpacity of Conv_oracle.level * Libnames.qualid Constrexpr.or_by_notation list
| VernacSetStrategy of (Conv_oracle.level * Libnames.qualid Constrexpr.or_by_notation list) list
| VernacMemOption of Goptions.option_name * Goptions.table_value list
| VernacPrintOption of Goptions.option_name
| VernacCheckMayEval of Genredexpr.raw_red_expr option * Goal_select.t option * Constrexpr.constr_expr
| VernacGlobalCheck of Constrexpr.constr_expr
| VernacDeclareReduction of string * Genredexpr.raw_red_expr
| VernacPrint of printable
| VernacSearch of searchable * Goal_select.t option * search_restriction
| VernacLocate of locatable
| VernacRegister of Libnames.qualid * register_kind
| VernacPrimitive of Constrexpr.ident_decl * CPrimitives.op_or_type * Constrexpr.constr_expr option
| VernacComments of comment list
| VernacAbort
| VernacAbortAll
| VernacRestart
| VernacUndo of int
| VernacUndoTo of int
| VernacFocus of int option
| VernacUnfocus
| VernacUnfocused
| VernacBullet of Proof_bullet.t
| VernacSubproof of Goal_select.t option
| VernacEndSubproof
| VernacShow of showable
| VernacCheckGuard
| VernacValidateProof
| VernacProof of Genarg.raw_generic_argument option * section_subset_expr option
| VernacAddOption of Goptions.option_name * Goptions.table_value list
| 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

Source

val synpure_vernac_expr_of_yojson : 
  Yojson.Safe.t ->
  synpure_vernac_expr Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_synpure_vernac_expr : 
  Ppx_hash_lib.Std.Hash.state ->
  synpure_vernac_expr ->
  Ppx_hash_lib.Std.Hash.state

Source

val hash_synpure_vernac_expr : 
  synpure_vernac_expr ->
  Ppx_hash_lib.Std.Hash.hash_value

Source

val compare_synpure_vernac_expr : 
  synpure_vernac_expr ->
  synpure_vernac_expr ->
  int

Sourcetype 'a vernac_expr_gen = 'a Vernacexpr.vernac_expr_gen =

| VernacSynterp of 'a
| VernacSynPure of synpure_vernac_expr

Source

val sexp_of_vernac_expr_gen : 
  ('a -> Sexplib0.Sexp.t) ->
  'a vernac_expr_gen ->
  Sexplib0.Sexp.t

Source

val vernac_expr_gen_of_sexp : 
  (Sexplib0.Sexp.t -> 'a) ->
  Sexplib0.Sexp.t ->
  'a vernac_expr_gen

Source

val vernac_expr_gen_to_yojson : 
  ('a -> Yojson.Safe.t) ->
  'a vernac_expr_gen ->
  Yojson.Safe.t

Source

val vernac_expr_gen_of_yojson : 
  (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  'a vernac_expr_gen Ppx_deriving_yojson_runtime.error_or

Source

val 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

Source

val compare_vernac_expr_gen : 
  ('a -> 'a -> int) ->
  'a vernac_expr_gen ->
  'a vernac_expr_gen ->
  int

Sourcetype control_flag = Vernacexpr.control_flag =

| ControlTime
| ControlRedirect of string
| ControlTimeout of int
| ControlFail
| 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

Source

val control_flag_of_yojson : 
  Yojson.Safe.t ->
  control_flag Ppx_deriving_yojson_runtime.error_or

Source

val 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 = {

control : 'a list;
attrs : Attributes.vernac_flags;
expr : 'b vernac_expr_gen;

}

Source

val sexp_of_vernac_control_gen_r : 
  ('a -> Sexplib0.Sexp.t) ->
  ('b -> Sexplib0.Sexp.t) ->
  ('a, 'b) vernac_control_gen_r ->
  Sexplib0.Sexp.t

Source

val vernac_control_gen_r_of_sexp : 
  (Sexplib0.Sexp.t -> 'a) ->
  (Sexplib0.Sexp.t -> 'b) ->
  Sexplib0.Sexp.t ->
  ('a, 'b) vernac_control_gen_r

Source

val vernac_control_gen_r_to_yojson : 
  ('a -> Yojson.Safe.t) ->
  ('b -> Yojson.Safe.t) ->
  ('a, 'b) vernac_control_gen_r ->
  Yojson.Safe.t

Source

val vernac_control_gen_r_of_yojson : 
  (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
  (Yojson.Safe.t -> 'b Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  ('a, 'b) vernac_control_gen_r Ppx_deriving_yojson_runtime.error_or

Source

val 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

Source

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

Sourcetype 'a vernac_control_gen = (control_flag, 'a) vernac_control_gen_r CAst.t

Source

val sexp_of_vernac_control_gen : 
  ('a -> Sexplib0.Sexp.t) ->
  'a vernac_control_gen ->
  Sexplib0.Sexp.t

Source

val vernac_control_gen_of_sexp : 
  (Sexplib0.Sexp.t -> 'a) ->
  Sexplib0.Sexp.t ->
  'a vernac_control_gen

Source

val vernac_control_gen_to_yojson : 
  ('a -> Yojson.Safe.t) ->
  'a vernac_control_gen ->
  Yojson.Safe.t

Source

val vernac_control_gen_of_yojson : 
  (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  'a vernac_control_gen Ppx_deriving_yojson_runtime.error_or

Source

val 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

Source

val compare_vernac_control_gen : 
  ('a -> 'a -> int) ->
  'a vernac_control_gen ->
  'a vernac_control_gen ->
  int

Sourcetype vernac_control = synterp_vernac_expr vernac_control_gen

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

Source

val vernac_control_of_yojson : 
  Yojson.Safe.t ->
  vernac_control Ppx_deriving_yojson_runtime.error_or

Source

val 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

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module `Serlib.Ser_vernacexpr`Source

package coq-lsp

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module Serlib.Ser_vernacexprSource

Module `Serlib.Ser_vernacexpr`Source