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