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_identifier = string
type scope_name = string
type goal_reference =
  1. | OpenSubgoals
  2. | NthGoal of int
  3. | GoalId of Names.Id.t
type printable =
  1. | PrintTypingFlags
  2. | PrintTables
  3. | PrintFullContext
  4. | PrintSectionContext of Libnames.qualid
  5. | PrintInspect of int
  6. | PrintGrammar of string
  7. | PrintCustomGrammar of string
  8. | PrintLoadPath of Names.DirPath.t option
  9. | PrintModules
  10. | PrintModule of Libnames.qualid
  11. | PrintModuleType of Libnames.qualid
  12. | PrintNamespace of Names.DirPath.t
  13. | PrintMLLoadPath
  14. | PrintMLModules
  15. | PrintDebugGC
  16. | PrintName of Libnames.qualid Constrexpr.or_by_notation * UnivNames.univ_name_list option
  17. | PrintGraph
  18. | PrintClasses
  19. | PrintTypeClasses
  20. | PrintInstances of Libnames.qualid Constrexpr.or_by_notation
  21. | PrintCoercions
  22. | PrintCoercionPaths of class_rawexpr * class_rawexpr
  23. | PrintCanonicalConversions of Libnames.qualid Constrexpr.or_by_notation list
  24. | PrintUniverses of bool * Libnames.qualid list option * string option
  25. | PrintHint of Libnames.qualid Constrexpr.or_by_notation
  26. | PrintHintGoal
  27. | PrintHintDbName of string
  28. | PrintHintDb
  29. | PrintScopes
  30. | PrintScope of string
  31. | PrintVisibility of string option
  32. | PrintAbout of Libnames.qualid Constrexpr.or_by_notation * UnivNames.univ_name_list option * Goal_select.t option
  33. | PrintImplicit of Libnames.qualid Constrexpr.or_by_notation
  34. | PrintAssumptions of bool * bool * Libnames.qualid Constrexpr.or_by_notation
  35. | PrintStrategy of Libnames.qualid Constrexpr.or_by_notation option
  36. | PrintRegistered
type glob_search_where =
  1. | InHyp
  2. | InConcl
  3. | Anywhere
type search_item =
  1. | SearchSubPattern of glob_search_where * bool * Constrexpr.constr_pattern_expr
  2. | SearchString of glob_search_where * bool * string * scope_name option
  3. | SearchKind of Decls.logical_kind
type search_request =
  1. | SearchLiteral of search_item
  2. | SearchDisjConj of (bool * search_request) list list
type searchable =
  1. | SearchPattern of Constrexpr.constr_pattern_expr
  2. | SearchRewrite of Constrexpr.constr_pattern_expr
  3. | SearchHead of Constrexpr.constr_pattern_expr
  4. | Search of (bool * search_request) 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. | ShowExistentials
  4. | ShowUniverses
  5. | ShowProofNames
  6. | ShowIntros of bool
  7. | ShowMatch of Libnames.qualid
type comment =
  1. | CommentConstr of Constrexpr.constr_expr
  2. | CommentString of string
  3. | CommentInt of int
type search_restriction =
  1. | SearchInside of Libnames.qualid list
  2. | SearchOutside of Libnames.qualid list
type verbose_flag = bool
type coercion_flag = bool
type instance_flag =
  1. | BackInstance
  2. | NoInstance
type export_flag = bool
type one_import_filter_name = Libnames.qualid * bool
type import_filter_expr =
  1. | ImportAll
  2. | ImportNames of one_import_filter_name list
type onlyparsing_flag = {
  1. onlyparsing : bool;
}
type locality_flag = bool
type option_setting =
  1. | OptionUnset
  2. | OptionSetTrue
  3. | OptionSetInt of int
  4. | OptionSetString of string
type syntax_modifier =
  1. | SetItemLevel of string list * Notation_term.constr_as_binder_kind option * Extend.production_level
  2. | SetLevel of int
  3. | SetCustomEntry of string * int option
  4. | SetAssoc of Gramlib.Gramext.g_assoc
  5. | SetEntryType of string * Extend.simple_constr_prod_entry_key
  6. | SetOnlyParsing
  7. | SetOnlyPrinting
  8. | SetFormat of string * Names.lstring
type decl_notation = {
  1. decl_ntn_string : Names.lstring;
  2. decl_ntn_interp : Constrexpr.constr_expr;
  3. decl_ntn_scope : scope_name option;
  4. decl_ntn_modifiers : syntax_modifier list;
}
type !'a fix_expr_gen = {
  1. fname : Names.lident;
  2. univs : Constrexpr.universe_decl_expr option;
  3. rec_order : 'a;
  4. binders : Constrexpr.local_binder_expr list;
  5. rtype : Constrexpr.constr_expr;
  6. body_def : Constrexpr.constr_expr option;
  7. notations : decl_notation list;
}
type fixpoint_expr = Constrexpr.recursion_order_expr option fix_expr_gen
type cofixpoint_expr = unit fix_expr_gen
type inductive_kind =
  1. | Inductive_kw
  2. | CoInductive
  3. | Variant
  4. | Record
  5. | Structure
  6. | Class of bool
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 record_field_attr = {
  1. rf_subclass : instance_flag;
  2. rf_priority : int option;
  3. rf_notation : decl_notation list;
  4. rf_canonical : bool;
}
type constructor_list_or_record_decl_expr =
  1. | Constructors of constructor_expr list
  2. | RecordDecl of Names.lident option * (local_decl_expr * record_field_attr) list
type inductive_params_expr = Constrexpr.local_binder_expr list * Constrexpr.local_binder_expr list option
and typeclass_context = typeclass_constraint list
type opacity_flag =
  1. | Opaque
  2. | Transparent
type proof_end =
  1. | Admitted
  2. | Proved of opacity_flag * Names.lident option
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 register_kind =
  1. | RegisterInline
  2. | RegisterCoqlib of Libnames.qualid
type module_binder = bool option * Names.lident list * module_ast_inl
type vernac_one_argument_status = {
  1. name : Names.Name.t;
  2. recarg_like : bool;
  3. notation_scope : string CAst.t option;
  4. implicit_status : Glob_term.binding_kind;
}
type vernac_argument_status =
  1. | VolatileArg
  2. | BidiArg
  3. | RealArg of vernac_one_argument_status
type arguments_modifier = [
  1. | `Assert
  2. | `ClearBidiHint
  3. | `ClearImplicits
  4. | `ClearScopes
  5. | `DefaultImplicits
  6. | `ExtraScopes
  7. | `ReductionDontExposeCase
  8. | `ReductionNeverUnfold
  9. | `Rename
]
type extend_name = string * int
type discharge =
  1. | DoDischarge
  2. | NoDischarge
type reference_or_constr =
  1. | HintsReference of Libnames.qualid
  2. | HintsConstr of Constrexpr.constr_expr
type hints_expr =
  1. | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
  2. | HintsResolveIFF of bool * Libnames.qualid list * int option
  3. | HintsImmediate of reference_or_constr list
  4. | HintsUnfold of Libnames.qualid list
  5. | HintsTransparency of Libnames.qualid Hints.hints_transparency_target * bool
  6. | HintsMode of Libnames.qualid * Hints.hint_mode list
  7. | HintsConstructors of Libnames.qualid list
  8. | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
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. | VernacDeclareScope of scope_name
  5. | VernacDelimiters of scope_name * string option
  6. | VernacBindScope of scope_name * class_rawexpr list
  7. | VernacInfix of Names.lstring * syntax_modifier list * Constrexpr.constr_expr * scope_name option
  8. | VernacNotation of Constrexpr.constr_expr * Names.lstring * syntax_modifier list * scope_name option
  9. | VernacNotationAddFormat of string * string * string
  10. | VernacDeclareCustomEntry of string
  11. | VernacDefinition of discharge * Decls.definition_object_kind * Constrexpr.name_decl * definition_expr
  12. | VernacStartTheoremProof of Decls.theorem_kind * proof_expr list
  13. | VernacEndProof of proof_end
  14. | VernacExactProof of Constrexpr.constr_expr
  15. | VernacAssumption of discharge * Decls.assumption_object_kind * Declaremods.inline * (Constrexpr.ident_decl list * Constrexpr.constr_expr) with_coercion list
  16. | VernacInductive of inductive_kind * (inductive_expr * decl_notation list) list
  17. | VernacFixpoint of discharge * fixpoint_expr list
  18. | VernacCoFixpoint of discharge * cofixpoint_expr list
  19. | VernacScheme of (Names.lident option * scheme) list
  20. | VernacCombinedScheme of Names.lident * Names.lident list
  21. | VernacUniverse of Names.lident list
  22. | VernacConstraint of Constrexpr.univ_constraint_expr list
  23. | VernacBeginSection of Names.lident
  24. | VernacEndSegment of Names.lident
  25. | VernacRequire of Libnames.qualid option * export_flag option * Libnames.qualid list
  26. | VernacImport of export_flag * (Libnames.qualid * import_filter_expr) list
  27. | VernacCanonical of Libnames.qualid Constrexpr.or_by_notation
  28. | VernacCoercion of Libnames.qualid Constrexpr.or_by_notation * class_rawexpr * class_rawexpr
  29. | VernacIdentityCoercion of Names.lident * class_rawexpr * class_rawexpr
  30. | VernacNameSectionHypSet of Names.lident * section_subset_expr
  31. | VernacInstance of Constrexpr.name_decl * Constrexpr.local_binder_expr list * Constrexpr.constr_expr * (bool * Constrexpr.constr_expr) option * hint_info_expr
  32. | VernacDeclareInstance of Constrexpr.ident_decl * Constrexpr.local_binder_expr list * Constrexpr.constr_expr * hint_info_expr
  33. | VernacContext of Constrexpr.local_binder_expr list
  34. | VernacExistingInstance of (Libnames.qualid * hint_info_expr) list
  35. | VernacExistingClass of Libnames.qualid
  36. | VernacDeclareModule of bool option * Names.lident * module_binder list * module_ast_inl
  37. | VernacDefineModule of bool option * Names.lident * module_binder list * module_ast_inl Declaremods.module_signature * module_ast_inl list
  38. | VernacDeclareModuleType of Names.lident * module_binder list * module_ast_inl list * module_ast_inl list
  39. | VernacInclude of module_ast_inl list
  40. | VernacSolveExistential of int * Constrexpr.constr_expr
  41. | VernacAddLoadPath of {
    1. implicit : bool;
    2. physical_path : CUnix.physical_path;
    3. logical_path : Names.DirPath.t;
    }
  42. | VernacRemoveLoadPath of string
  43. | VernacAddMLPath of string
  44. | VernacDeclareMLModule of string list
  45. | VernacChdir of string option
  46. | VernacWriteState of string
  47. | VernacRestoreState of string
  48. | VernacResetName of Names.lident
  49. | VernacResetInitial
  50. | VernacBack of int
  51. | VernacCreateHintDb of string * bool
  52. | VernacRemoveHints of string list * Libnames.qualid list
  53. | VernacHints of string list * hints_expr
  54. | VernacSyntacticDefinition of Names.lident * Names.Id.t list * Constrexpr.constr_expr * onlyparsing_flag
  55. | VernacArguments of Libnames.qualid Constrexpr.or_by_notation * vernac_argument_status list * (Names.Name.t * Glob_term.binding_kind) list list * arguments_modifier list
  56. | VernacReserve of simple_binder list
  57. | VernacGeneralizable of Names.lident list option
  58. | VernacSetOpacity of Conv_oracle.level * Libnames.qualid Constrexpr.or_by_notation list
  59. | VernacSetStrategy of (Conv_oracle.level * Libnames.qualid Constrexpr.or_by_notation list) list
  60. | VernacSetOption of bool * Goptions.option_name * option_setting
  61. | VernacAddOption of Goptions.option_name * Goptions.table_value list
  62. | VernacRemoveOption of Goptions.option_name * Goptions.table_value list
  63. | VernacMemOption of Goptions.option_name * Goptions.table_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 Libnames.qualid * register_kind
  72. | VernacPrimitive of Constrexpr.ident_decl * CPrimitives.op_or_type * Constrexpr.constr_expr option
  73. | VernacComments of comment list
  74. | VernacAbort of Names.lident option
  75. | VernacAbortAll
  76. | VernacRestart
  77. | VernacUndo of int
  78. | VernacUndoTo of int
  79. | VernacFocus of int option
  80. | VernacUnfocus
  81. | VernacUnfocused
  82. | VernacBullet of Proof_bullet.t
  83. | VernacSubproof of Goal_select.t option
  84. | VernacEndSubproof
  85. | VernacShow of showable
  86. | VernacCheckGuard
  87. | VernacProof of Genarg.raw_generic_argument option * section_subset_expr option
  88. | VernacProofMode of string
  89. | VernacExtend of extend_name * Genarg.raw_generic_argument list
type control_flag =
  1. | ControlTime of bool
  2. | ControlRedirect of string
  3. | ControlTimeout of int
  4. | ControlFail
type vernac_control_r = {
  1. control : control_flag list;
  2. attrs : Attributes.vernac_flags;
  3. expr : vernac_expr;
}
and vernac_control = vernac_control_r CAst.t