package coq

  1. Overview
  2. Docs
Package contains no libraries
type lident = Names.Id.t Loc.located
type lstring = string Loc.located
type class_rawexpr =
  1. | FunClass
  2. | SortClass
  3. | RefClass of Libnames.reference Misctypes.or_by_notation
type goal_selector =
  1. | SelectNth of int
  2. | SelectList of (int * int) list
  3. | SelectId of Names.Id.t
  4. | SelectAll
type goal_identifier = string
type scope_name = string
type goal_reference =
  1. | OpenSubgoals
  2. | NthGoal of int
  3. | GoalId of Names.Id.t
  4. | GoalUid of goal_identifier
type printable =
  1. | PrintTables
  2. | PrintFullContext
  3. | PrintSectionContext of Libnames.reference
  4. | PrintInspect of int
  5. | PrintGrammar of string
  6. | PrintLoadPath of Names.DirPath.t option
  7. | PrintModules
  8. | PrintModule of Libnames.reference
  9. | PrintModuleType of Libnames.reference
  10. | PrintNamespace of Names.DirPath.t
  11. | PrintMLLoadPath
  12. | PrintMLModules
  13. | PrintDebugGC
  14. | PrintName of Libnames.reference Misctypes.or_by_notation
  15. | PrintGraph
  16. | PrintClasses
  17. | PrintTypeClasses
  18. | PrintInstances of Libnames.reference Misctypes.or_by_notation
  19. | PrintCoercions
  20. | PrintCoercionPaths of class_rawexpr * class_rawexpr
  21. | PrintCanonicalConversions
  22. | PrintUniverses of bool * string option
  23. | PrintHint of Libnames.reference Misctypes.or_by_notation
  24. | PrintHintGoal
  25. | PrintHintDbName of string
  26. | PrintHintDb
  27. | PrintScopes
  28. | PrintScope of string
  29. | PrintVisibility of string option
  30. | PrintAbout of Libnames.reference Misctypes.or_by_notation * goal_selector option
  31. | PrintImplicit of Libnames.reference Misctypes.or_by_notation
  32. | PrintAssumptions of bool * bool * Libnames.reference Misctypes.or_by_notation
  33. | PrintStrategy of Libnames.reference Misctypes.or_by_notation option
type search_about_item =
  1. | SearchSubPattern of Constrexpr.constr_pattern_expr
  2. | SearchString of string * scope_name option
type searchable =
  1. | SearchPattern of Constrexpr.constr_pattern_expr
  2. | SearchRewrite of Constrexpr.constr_pattern_expr
  3. | SearchHead of Constrexpr.constr_pattern_expr
  4. | SearchAbout of (bool * search_about_item) list
type locatable =
  1. | LocateAny of Libnames.reference Misctypes.or_by_notation
  2. | LocateTerm of Libnames.reference Misctypes.or_by_notation
  3. | LocateLibrary of Libnames.reference
  4. | LocateModule of Libnames.reference
  5. | LocateTactic of Libnames.reference
  6. | LocateFile of string
type showable =
  1. | ShowGoal of goal_reference
  2. | ShowProof
  3. | ShowScript
  4. | ShowExistentials
  5. | ShowUniverses
  6. | ShowProofNames
  7. | ShowIntros of bool
  8. | ShowMatch of Libnames.reference
type comment =
  1. | CommentConstr of Constrexpr.constr_expr
  2. | CommentString of string
  3. | CommentInt of int
type reference_or_constr =
  1. | HintsReference of Libnames.reference
  2. | HintsConstr of Constrexpr.constr_expr
type hint_mode =
  1. | ModeInput
  2. | ModeNoHeadEvar
  3. | ModeOutput
type !'a hint_info_gen = {
  1. hint_priority : int option;
  2. hint_pattern : 'a option;
}
type hints_expr =
  1. | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
  2. | HintsImmediate of reference_or_constr list
  3. | HintsUnfold of Libnames.reference list
  4. | HintsTransparency of Libnames.reference list * bool
  5. | HintsMode of Libnames.reference * hint_mode list
  6. | HintsConstructors of Libnames.reference list
  7. | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
type search_restriction =
  1. | SearchInside of Libnames.reference list
  2. | SearchOutside of Libnames.reference list
type rec_flag = bool
type verbose_flag = bool
type opacity_flag =
  1. | Opaque of lident list option
  2. | Transparent
type coercion_flag = bool
type instance_flag = bool option
type export_flag = bool
type inductive_flag = Decl_kinds.recursivity_kind
type onlyparsing_flag = Flags.compat_version option
type locality_flag = bool
type obsolete_locality = bool
type option_value = Goptions.option_value =
  1. | BoolValue of bool
  2. | IntValue of int option
  3. | StringValue of string
  4. | StringOptValue of string option
type option_ref_value =
  1. | StringRefValue of string
  2. | QualidRefValue of Libnames.reference
type plident = lident * lident list option
type sort_expr = Misctypes.glob_sort
type local_decl_expr =
  1. | AssumExpr of lname * Constrexpr.constr_expr
  2. | DefExpr of lname * Constrexpr.constr_expr * Constrexpr.constr_expr option
type inductive_kind =
  1. | Inductive_kw
  2. | CoInductive
  3. | Variant
  4. | Record
  5. | Structure
  6. | Class of bool
type decl_notation = lstring * Constrexpr.constr_expr * scope_name option
type simple_binder = lident list * Constrexpr.constr_expr
type class_binder = lident * Constrexpr.constr_expr list
type !'a with_coercion = coercion_flag * 'a
type !'a with_instance = instance_flag * 'a
type !'a with_notation = 'a * decl_notation list
type !'a with_priority = 'a * int option
type constructor_expr = (lident * Constrexpr.constr_expr) with_coercion
type constructor_list_or_record_decl_expr =
  1. | Constructors of constructor_expr list
  2. | RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list
type one_inductive_expr = plident * Constrexpr.local_binder_expr list * Constrexpr.constr_expr option * constructor_expr list
type proof_expr = plident option * (Constrexpr.local_binder_expr list * Constrexpr.constr_expr)
type syntax_modifier =
  1. | SetItemLevel of string list * Extend.production_level
  2. | SetLevel of int
  3. | SetAssoc of Extend.gram_assoc
  4. | SetEntryType of string * Extend.simple_constr_prod_entry_key
  5. | SetOnlyParsing
  6. | SetOnlyPrinting
  7. | SetCompatVersion of Flags.compat_version
  8. | SetFormat of string * string Loc.located
type proof_end =
  1. | Admitted
  2. | Proved of opacity_flag * lident option
type section_subset_expr =
  1. | SsEmpty
  2. | SsSingl of lident
  3. | SsCompl of section_subset_expr
  4. | SsUnion of section_subset_expr * section_subset_expr
  5. | SsSubstr of section_subset_expr * section_subset_expr
  6. | SsFwdClose of section_subset_expr
type extend_name = string * int
type register_kind =
  1. | RegisterInline
type bullet =
  1. | Dash of int
  2. | Star of int
  3. | Plus of int
type stm_vernac =
  1. | JoinDocument
  2. | Wait
type !'a module_signature =
  1. | Enforce of 'a
  2. | Check of 'a list
type inline =
  1. | NoInline
  2. | DefaultInline
  3. | InlineAt of int
type module_ast_inl = Constrexpr.module_ast * inline
type module_binder = bool option * lident list * module_ast_inl
type cumulative_inductive_parsing_flag =
  1. | GlobalCumulativity
  2. | GlobalNonCumulativity
  3. | LocalCumulativity
  4. | LocalNonCumulativity
type vernac_expr =
  1. | VernacLoad of verbose_flag * string
  2. | VernacTime of vernac_expr Loc.located
  3. | VernacRedirect of string * vernac_expr Loc.located
  4. | VernacTimeout of int * vernac_expr
  5. | VernacFail of vernac_expr
  6. | VernacSyntaxExtension of obsolete_locality * lstring * syntax_modifier list
  7. | VernacOpenCloseScope of obsolete_locality * bool * scope_name
  8. | VernacDelimiters of scope_name * string option
  9. | VernacBindScope of scope_name * class_rawexpr list
  10. | VernacInfix of obsolete_locality * lstring * syntax_modifier list * Constrexpr.constr_expr * scope_name option
  11. | VernacNotation of obsolete_locality * Constrexpr.constr_expr * lstring * syntax_modifier list * scope_name option
  12. | VernacNotationAddFormat of string * string * string
  13. | VernacDefinition of Decl_kinds.locality option * Decl_kinds.definition_object_kind * plident * definition_expr
  14. | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list
  15. | VernacEndProof of proof_end
  16. | VernacExactProof of Constrexpr.constr_expr
  17. | VernacAssumption of Decl_kinds.locality option * Decl_kinds.assumption_object_kind * inline * (plident list * Constrexpr.constr_expr) with_coercion list
  18. | VernacInductive of cumulative_inductive_parsing_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list
  19. | VernacFixpoint of Decl_kinds.locality option * (fixpoint_expr * decl_notation list) list
  20. | VernacCoFixpoint of Decl_kinds.locality option * (cofixpoint_expr * decl_notation list) list
  21. | VernacScheme of (lident option * scheme) list
  22. | VernacCombinedScheme of lident * lident list
  23. | VernacUniverse of lident list
  24. | VernacConstraint of (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list
  25. | VernacBeginSection of lident
  26. | VernacEndSegment of lident
  27. | VernacRequire of Libnames.reference option * export_flag option * Libnames.reference list
  28. | VernacImport of export_flag * Libnames.reference list
  29. | VernacCanonical of Libnames.reference Misctypes.or_by_notation
  30. | VernacCoercion of obsolete_locality * Libnames.reference Misctypes.or_by_notation * class_rawexpr * class_rawexpr
  31. | VernacIdentityCoercion of obsolete_locality * lident * class_rawexpr * class_rawexpr
  32. | VernacNameSectionHypSet of lident * section_subset_expr
  33. | VernacInstance of bool * Constrexpr.local_binder_expr list * Constrexpr.typeclass_constraint * (bool * Constrexpr.constr_expr) option * hint_info_expr
  34. | VernacContext of Constrexpr.local_binder_expr list
  35. | VernacDeclareInstances of (Libnames.reference * hint_info_expr) list
  36. | VernacDeclareClass of Libnames.reference
  37. | VernacDeclareModule of bool option * lident * module_binder list * module_ast_inl
  38. | VernacDefineModule of bool option * lident * module_binder list * module_ast_inl module_signature * module_ast_inl list
  39. | VernacDeclareModuleType of lident * module_binder list * module_ast_inl list * module_ast_inl list
  40. | VernacInclude of module_ast_inl list
  41. | VernacSolveExistential of int * Constrexpr.constr_expr
  42. | VernacAddLoadPath of rec_flag * string * Names.DirPath.t option
  43. | VernacRemoveLoadPath of string
  44. | VernacAddMLPath of rec_flag * string
  45. | VernacDeclareMLModule of string list
  46. | VernacChdir of string option
  47. | VernacWriteState of string
  48. | VernacRestoreState of string
  49. | VernacResetName of lident
  50. | VernacResetInitial
  51. | VernacBack of int
  52. | VernacBackTo of int
  53. | VernacCreateHintDb of string * bool
  54. | VernacRemoveHints of string list * Libnames.reference list
  55. | VernacHints of obsolete_locality * string list * hints_expr
  56. | VernacSyntacticDefinition of Names.Id.t Loc.located * Names.Id.t list * Constrexpr.constr_expr * obsolete_locality * onlyparsing_flag
  57. | VernacDeclareImplicits of Libnames.reference Misctypes.or_by_notation * (Constrexpr.explicitation * bool * bool) list list
  58. | VernacArguments of Libnames.reference Misctypes.or_by_notation * vernac_argument_status list * (Names.Name.t * vernac_implicit_status) list list * int option * [ `Assert | `ClearImplicits | `ClearScopes | `DefaultImplicits | `ExtraScopes | `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename ] list
  59. | VernacArgumentsScope of Libnames.reference Misctypes.or_by_notation * scope_name option list
  60. | VernacReserve of simple_binder list
  61. | VernacGeneralizable of lident list option
  62. | VernacSetOpacity of Conv_oracle.level * Libnames.reference Misctypes.or_by_notation list
  63. | VernacSetStrategy of (Conv_oracle.level * Libnames.reference Misctypes.or_by_notation list) list
  64. | VernacUnsetOption of Goptions.option_name
  65. | VernacSetOption of Goptions.option_name * option_value
  66. | VernacSetAppendOption of Goptions.option_name * string
  67. | VernacAddOption of Goptions.option_name * option_ref_value list
  68. | VernacRemoveOption of Goptions.option_name * option_ref_value list
  69. | VernacMemOption of Goptions.option_name * option_ref_value list
  70. | VernacPrintOption of Goptions.option_name
  71. | VernacCheckMayEval of Genredexpr.raw_red_expr option * goal_selector option * Constrexpr.constr_expr
  72. | VernacGlobalCheck of Constrexpr.constr_expr
  73. | VernacDeclareReduction of string * Genredexpr.raw_red_expr
  74. | VernacPrint of printable
  75. | VernacSearch of searchable * goal_selector option * search_restriction
  76. | VernacLocate of locatable
  77. | VernacRegister of lident * register_kind
  78. | VernacComments of comment list
  79. | VernacStm of stm_vernac
  80. | VernacGoal of Constrexpr.constr_expr
  81. | VernacAbort of lident option
  82. | VernacAbortAll
  83. | VernacRestart
  84. | VernacUndo of int
  85. | VernacUndoTo of int
  86. | VernacBacktrack of int * int * int
  87. | VernacFocus of int option
  88. | VernacUnfocus
  89. | VernacUnfocused
  90. | VernacBullet of bullet
  91. | VernacSubproof of int option
  92. | VernacEndSubproof
  93. | VernacShow of showable
  94. | VernacCheckGuard
  95. | VernacProof of Genarg.raw_generic_argument option * section_subset_expr option
  96. | VernacProofMode of string
  97. | VernacToplevelControl of exn
  98. | VernacExtend of extend_name * Genarg.raw_generic_argument list
  99. | VernacProgram of vernac_expr
  100. | VernacPolymorphic of bool * vernac_expr
  101. | VernacLocal of bool * vernac_expr
and vernac_implicit_status =
  1. | Implicit
  2. | MaximallyImplicit
  3. | NotImplicit
and vernac_argument_status = {
  1. name : Names.Name.t;
  2. recarg_like : bool;
  3. notation_scope : string Loc.located option;
  4. implicit_status : vernac_implicit_status;
}
type vernac_type =
  1. | VtStartProof of vernac_start
  2. | VtSideff of vernac_sideff_type
  3. | VtQed of vernac_qed_type
  4. | VtProofStep of proof_step
  5. | VtProofMode of string
  6. | VtQuery of vernac_part_of_script * Feedback.route_id
  7. | VtStm of vernac_control * vernac_part_of_script
  8. | VtUnknown
and vernac_qed_type =
  1. | VtKeep
  2. | VtKeepAsAxiom
  3. | VtDrop
and vernac_start = string * opacity_guarantee * Names.Id.t list
and vernac_sideff_type = Names.Id.t list
and vernac_part_of_script = bool
and vernac_control =
  1. | VtWait
  2. | VtJoinDocument
  3. | VtBack of Stateid.t
and opacity_guarantee =
  1. | GuaranteesOpacity
  2. | Doesn'tGuaranteeOpacity
and proof_step = {
  1. parallel : [ `No | `Yes of solving_tac * anon_abstracting_tac ];
  2. proof_block_detection : proof_block_name option;
}
and solving_tac = bool
and anon_abstracting_tac = bool
and proof_block_name = string
type vernac_when =
  1. | VtNow
  2. | VtLater
type vernac_classification = vernac_type * vernac_when
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct