package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type class_rawexpr =
  1. | FunClass
  2. | SortClass
  3. | RefClass of Libnames.qualid Constrexpr.or_by_notation
type goal_selector = Goal_select.t =
  1. | SelectAlreadyFocused
    (*
    • deprecated Use Goal_select.SelectAlreadyFocused
    *)
  2. | SelectNth of int
    (*
    • deprecated Use Goal_select.SelectNth
    *)
  3. | SelectList of (int * int) list
    (*
    • deprecated Use Goal_select.SelectList
    *)
  4. | SelectId of Names.Id.t
    (*
    • deprecated Use Goal_select.SelectId
    *)
  5. | SelectAll
    (*
    • deprecated Use Goal_select.SelectAll
    *)
  • deprecated Use Goal_select.t
type goal_identifier = string
type scope_name = string
type goal_reference =
  1. | OpenSubgoals
  2. | NthGoal of int
  3. | GoalId of Names.Id.t
type univ_name_list = UnivNames.univ_name_list
  • deprecated Use [UnivNames.univ_name_list]
type printable =
  1. | PrintTables
  2. | PrintFullContext
  3. | PrintSectionContext of Libnames.qualid
  4. | PrintInspect of int
  5. | PrintGrammar of string
  6. | PrintLoadPath of Names.DirPath.t option
  7. | PrintModules
  8. | PrintModule of Libnames.qualid
  9. | PrintModuleType of Libnames.qualid
  10. | PrintNamespace of Names.DirPath.t
  11. | PrintMLLoadPath
  12. | PrintMLModules
  13. | PrintDebugGC
  14. | PrintName of Libnames.qualid Constrexpr.or_by_notation * UnivNames.univ_name_list option
  15. | PrintGraph
  16. | PrintClasses
  17. | PrintTypeClasses
  18. | PrintInstances of Libnames.qualid Constrexpr.or_by_notation
  19. | PrintCoercions
  20. | PrintCoercionPaths of class_rawexpr * class_rawexpr
  21. | PrintCanonicalConversions
  22. | PrintUniverses of bool * string option
  23. | PrintHint of Libnames.qualid Constrexpr.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.qualid Constrexpr.or_by_notation * UnivNames.univ_name_list option * Goal_select.t option
  31. | PrintImplicit of Libnames.qualid Constrexpr.or_by_notation
  32. | PrintAssumptions of bool * bool * Libnames.qualid Constrexpr.or_by_notation
  33. | PrintStrategy of Libnames.qualid Constrexpr.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.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
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.qualid
type comment =
  1. | CommentConstr of Constrexpr.constr_expr
  2. | CommentString of string
  3. | CommentInt of int
type reference_or_constr = Hints.reference_or_constr =
  1. | HintsReference of Libnames.qualid
    (*
    • deprecated Use Hints.HintsReference
    *)
  2. | HintsConstr of Constrexpr.constr_expr
    (*
    • deprecated Use Hints.HintsConstr
    *)
  • deprecated Please use [Hints.reference_or_constr]
type hint_mode = Hints.hint_mode =
  1. | ModeInput
    (*
    • deprecated Use Hints.ModeInput
    *)
  2. | ModeNoHeadEvar
    (*
    • deprecated Use Hints.ModeNoHeadEvar
    *)
  3. | ModeOutput
    (*
    • deprecated Use Hints.ModeOutput
    *)
  • deprecated Please use [Hints.hint_mode]
type !'a hint_info_gen = 'a Typeclasses.hint_info_gen = {
  1. hint_priority : int option;
    (*
    • deprecated Use Typeclasses.hint_priority
    *)
  2. hint_pattern : 'a option;
    (*
    • deprecated Use Typeclasses.hint_pattern
    *)
}
  • deprecated Please use [Typeclasses.hint_info_gen]
type hint_info_expr = Hints.hint_info_expr
  • deprecated Please use [Hints.hint_info_expr]
type hints_expr = Hints.hints_expr =
  1. | HintsResolve of (Hints.hint_info_expr * bool * Hints.reference_or_constr) list
    (*
    • deprecated Use the constructor in module [Hints]
    *)
  2. | HintsResolveIFF of bool * Libnames.qualid list * int option
    (*
    • deprecated Use the constructor in module [Hints]
    *)
  3. | HintsImmediate of Hints.reference_or_constr list
    (*
    • deprecated Use the constructor in module [Hints]
    *)
  4. | HintsUnfold of Libnames.qualid list
    (*
    • deprecated Use the constructor in module [Hints]
    *)
  5. | HintsTransparency of Libnames.qualid Hints.hints_transparency_target * bool
    (*
    • deprecated Use the constructor in module [Hints]
    *)
  6. | HintsMode of Libnames.qualid * Hints.hint_mode list
    (*
    • deprecated Use the constructor in module [Hints]
    *)
  7. | HintsConstructors of Libnames.qualid list
    (*
    • deprecated Use the constructor in module [Hints]
    *)
  8. | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
    (*
    • deprecated Use the constructor in module [Hints]
    *)
  • deprecated Please use [Hints.hints_expr]
type search_restriction =
  1. | SearchInside of Libnames.qualid list
  2. | SearchOutside of Libnames.qualid list
type rec_flag = bool
type verbose_flag = bool
type opacity_flag = Proof_global.opacity_flag =
  1. | Opaque
    (*
    • deprecated Use Proof_global.Opaque
    *)
  2. | Transparent
    (*
    • deprecated Use Proof_global.Transparent
    • deprecated Please use [Proof_global.opacity_flag]
    *)
type coercion_flag = bool
type instance_flag = bool option
type export_flag = bool
type inductive_flag = Declarations.recursivity_kind
type onlyparsing_flag = Flags.compat_version option
type locality_flag = 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.qualid
type sort_expr = Sorts.family
type local_decl_expr =
  1. | AssumExpr of Names.lname * Constrexpr.constr_expr
  2. | DefExpr of Names.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 = Names.lstring * Constrexpr.constr_expr * scope_name option
type simple_binder = Names.lident list * Constrexpr.constr_expr
type class_binder = Names.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_list_or_record_decl_expr =
  1. | Constructors of constructor_expr list
  2. | RecordDecl of Names.lident option * local_decl_expr with_instance with_priority with_notation list
and typeclass_context = typeclass_constraint list
type syntax_modifier =
  1. | SetItemLevel of string list * Notation_term.constr_as_binder_kind option * Extend.production_level option
  2. | SetLevel of int
  3. | SetCustomEntry of string * int option
  4. | SetAssoc of Extend.gram_assoc
  5. | SetEntryType of string * Extend.simple_constr_prod_entry_key
  6. | SetOnlyParsing
  7. | SetOnlyPrinting
  8. | SetCompatVersion of Flags.compat_version
  9. | SetFormat of string * Names.lstring
type proof_end =
  1. | Admitted
  2. | Proved of Proof_global.opacity_flag * Names.lident option
type scheme =
  1. | InductionScheme of bool * Libnames.qualid Constrexpr.or_by_notation * sort_expr
  2. | CaseScheme of bool * Libnames.qualid Constrexpr.or_by_notation * sort_expr
  3. | EqualityScheme of Libnames.qualid Constrexpr.or_by_notation
type 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
type extend_name = string * int
type register_kind =
  1. | RegisterInline
type bullet = Proof_bullet.t
  • deprecated Alias type, please use [Proof_bullet.t]
type !'a module_signature = 'a Declaremods.module_signature =
  1. | Enforce of 'a
    (*
    • deprecated Use the constructor in module [Declaremods]
    *)
  2. | Check of 'a list
    (*
    • deprecated Use the constructor in module [Declaremods]
    *)
  • deprecated please use [Declaremods.module_signature].
type inline = Declaremods.inline =
  1. | NoInline
    (*
    • deprecated Use the constructor in module [Declaremods]
    *)
  2. | DefaultInline
    (*
    • deprecated Use the constructor in module [Declaremods]
    *)
  3. | InlineAt of int
    (*
    • deprecated Use the constructor in module [Declaremods]
    *)
  • deprecated please use [Declaremods.inline].
type module_binder = bool option * Names.lident list * module_ast_inl
type vernac_cumulative =
  1. | VernacCumulative
  2. | VernacNonCumulative
type vernac_implicit_status =
  1. | Implicit
  2. | MaximallyImplicit
  3. | NotImplicit
type vernac_argument_status = {
  1. name : Names.Name.t;
  2. recarg_like : bool;
  3. notation_scope : string CAst.t option;
  4. implicit_status : vernac_implicit_status;
}
type nonrec vernac_expr =
  1. | VernacLoad of verbose_flag * string
  2. | VernacSyntaxExtension of bool * Names.lstring * syntax_modifier list
  3. | VernacOpenCloseScope of bool * scope_name
  4. | VernacDelimiters of scope_name * string option
  5. | VernacBindScope of scope_name * class_rawexpr list
  6. | VernacInfix of Names.lstring * syntax_modifier list * Constrexpr.constr_expr * scope_name option
  7. | VernacNotation of Constrexpr.constr_expr * Names.lstring * syntax_modifier list * scope_name option
  8. | VernacNotationAddFormat of string * string * string
  9. | VernacDeclareCustomEntry of string
  10. | VernacDefinition of Decl_kinds.discharge * Decl_kinds.definition_object_kind * Constrexpr.name_decl * definition_expr
  11. | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list
  12. | VernacEndProof of proof_end
  13. | VernacExactProof of Constrexpr.constr_expr
  14. | VernacAssumption of Decl_kinds.discharge * Decl_kinds.assumption_object_kind * Declaremods.inline * (Constrexpr.ident_decl list * Constrexpr.constr_expr) with_coercion list
  15. | VernacInductive of vernac_cumulative option * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list
  16. | VernacFixpoint of Decl_kinds.discharge * (fixpoint_expr * decl_notation list) list
  17. | VernacCoFixpoint of Decl_kinds.discharge * (cofixpoint_expr * decl_notation list) list
  18. | VernacScheme of (Names.lident option * scheme) list
  19. | VernacCombinedScheme of Names.lident * Names.lident list
  20. | VernacUniverse of Names.lident list
  21. | VernacConstraint of Glob_term.glob_constraint list
  22. | VernacBeginSection of Names.lident
  23. | VernacEndSegment of Names.lident
  24. | VernacRequire of Libnames.qualid option * export_flag option * Libnames.qualid list
  25. | VernacImport of export_flag * Libnames.qualid list
  26. | VernacCanonical of Libnames.qualid Constrexpr.or_by_notation
  27. | VernacCoercion of Libnames.qualid Constrexpr.or_by_notation * class_rawexpr * class_rawexpr
  28. | VernacIdentityCoercion of Names.lident * class_rawexpr * class_rawexpr
  29. | VernacNameSectionHypSet of Names.lident * section_subset_expr
  30. | VernacInstance of bool * Constrexpr.local_binder_expr list * typeclass_constraint * (bool * Constrexpr.constr_expr) option * Hints.hint_info_expr
  31. | VernacContext of Constrexpr.local_binder_expr list
  32. | VernacDeclareInstances of (Libnames.qualid * Hints.hint_info_expr) list
  33. | VernacDeclareClass of Libnames.qualid
  34. | VernacDeclareModule of bool option * Names.lident * module_binder list * module_ast_inl
  35. | VernacDefineModule of bool option * Names.lident * module_binder list * module_ast_inl Declaremods.module_signature * module_ast_inl list
  36. | VernacDeclareModuleType of Names.lident * module_binder list * module_ast_inl list * module_ast_inl list
  37. | VernacInclude of module_ast_inl list
  38. | VernacSolveExistential of int * Constrexpr.constr_expr
  39. | VernacAddLoadPath of rec_flag * string * Names.DirPath.t option
  40. | VernacRemoveLoadPath of string
  41. | VernacAddMLPath of rec_flag * string
  42. | VernacDeclareMLModule of string list
  43. | VernacChdir of string option
  44. | VernacWriteState of string
  45. | VernacRestoreState of string
  46. | VernacResetName of Names.lident
  47. | VernacResetInitial
  48. | VernacBack of int
  49. | VernacBackTo of int
  50. | VernacCreateHintDb of string * bool
  51. | VernacRemoveHints of string list * Libnames.qualid list
  52. | VernacHints of string list * Hints.hints_expr
  53. | VernacSyntacticDefinition of Names.lident * Names.Id.t list * Constrexpr.constr_expr * onlyparsing_flag
  54. | VernacArguments of Libnames.qualid Constrexpr.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
  55. | VernacReserve of simple_binder list
  56. | VernacGeneralizable of Names.lident list option
  57. | VernacSetOpacity of Conv_oracle.level * Libnames.qualid Constrexpr.or_by_notation list
  58. | VernacSetStrategy of (Conv_oracle.level * Libnames.qualid Constrexpr.or_by_notation list) list
  59. | VernacUnsetOption of export_flag * Goptions.option_name
  60. | VernacSetOption of export_flag * Goptions.option_name * option_value
  61. | VernacAddOption of Goptions.option_name * option_ref_value list
  62. | VernacRemoveOption of Goptions.option_name * option_ref_value list
  63. | VernacMemOption of Goptions.option_name * option_ref_value list
  64. | VernacPrintOption of Goptions.option_name
  65. | VernacCheckMayEval of Genredexpr.raw_red_expr option * Goal_select.t option * Constrexpr.constr_expr
  66. | VernacGlobalCheck of Constrexpr.constr_expr
  67. | VernacDeclareReduction of string * Genredexpr.raw_red_expr
  68. | VernacPrint of printable
  69. | VernacSearch of searchable * Goal_select.t option * search_restriction
  70. | VernacLocate of locatable
  71. | VernacRegister of Names.lident * register_kind
  72. | VernacComments of comment list
  73. | VernacAbort of Names.lident option
  74. | VernacAbortAll
  75. | VernacRestart
  76. | VernacUndo of int
  77. | VernacUndoTo of int
  78. | VernacFocus of int option
  79. | VernacUnfocus
  80. | VernacUnfocused
  81. | VernacBullet of Proof_bullet.t
  82. | VernacSubproof of Goal_select.t option
  83. | VernacEndSubproof
  84. | VernacShow of showable
  85. | VernacCheckGuard
  86. | VernacProof of Genarg.raw_generic_argument option * section_subset_expr option
  87. | VernacProofMode of string
  88. | VernacExtend of extend_name * Genarg.raw_generic_argument list
type vernac_flags = (string * vernac_flag_value) list
and vernac_flag_value =
  1. | VernacFlagEmpty
  2. | VernacFlagLeaf of string
  3. | VernacFlagList of vernac_flags
type vernac_control =
  1. | VernacExpr of vernac_flags * vernac_expr
  2. | VernacTime of bool * vernac_control CAst.t
  3. | VernacRedirect of string * vernac_control CAst.t
  4. | VernacTimeout of int * vernac_control
  5. | VernacFail of vernac_control
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
  7. | VtMeta
  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 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