Module Vernacexpr

type class_rawexpr =
| FunClass
| SortClass
| RefClass of Libnames.qualid Constrexpr.or_by_notation

Vernac expressions, produced by the parser

type goal_identifier = string
type scope_name = string
type goal_reference =
| OpenSubgoals
| NthGoal of int
| GoalId of Names.Id.t
type printable =
| PrintTypingFlags
| PrintTables
| PrintFullContext
| PrintSectionContext of Libnames.qualid
| PrintInspect of int
| PrintGrammar of string
| PrintCustomGrammar of string
| 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 class_rawexpr * class_rawexpr
| 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
type glob_search_where =
| InHyp
| InConcl
| Anywhere
type 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
type search_request =
| SearchLiteral of search_item
| SearchDisjConj of (bool * search_request) list list
type searchable =
| SearchPattern of Constrexpr.constr_pattern_expr
| SearchRewrite of Constrexpr.constr_pattern_expr
| Search of (bool * search_request) list
type 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
type showable =
| ShowGoal of goal_reference
| ShowProof
| ShowExistentials
| ShowUniverses
| ShowProofNames
| ShowIntros of bool
| ShowMatch of Libnames.qualid
type comment =
| CommentConstr of Constrexpr.constr_expr
| CommentString of string
| CommentInt of int
type search_restriction =
| SearchInside of Libnames.qualid list
| SearchOutside of Libnames.qualid list
type verbose_flag = bool
type coercion_flag = bool
type instance_flag =
| BackInstance
| NoInstance
type export_flag = Lib.export_flag =
| Export
| Import
type import_categories = {
negative : bool;
import_cats : string CAst.t list;
}
type export_with_cats = export_flag * import_categories option
type infix_flag = bool
type one_import_filter_name = Libnames.qualid * bool
type import_filter_expr =
| ImportAll
| ImportNames of one_import_filter_name list
type locality_flag = bool
type option_setting =
| OptionUnset
| OptionSetTrue
| OptionSetInt of int
| OptionSetString of string
type 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
type notation_format =
| TextFormat of Names.lstring
| ExtraFormat of string * Names.lstring
type syntax_modifier =
| SetItemLevel of string list * Notation_term.constr_as_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
type decl_notation = {
decl_ntn_string : Names.lstring;
decl_ntn_interp : Constrexpr.constr_expr;
decl_ntn_scope : scope_name option;
decl_ntn_modifiers : syntax_modifier CAst.t list;
}
type 'a 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 : decl_notation list;
}
type fixpoint_expr = Constrexpr.recursion_order_expr option fix_expr_gen
type cofixpoint_expr = unit fix_expr_gen
type 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
type inductive_kind =
| Inductive_kw
| CoInductive
| Variant
| Record
| Structure
| 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 = {
rf_subclass : instance_flag;
rf_reverse : bool option;
rf_priority : int option;
rf_notation : decl_notation list;
rf_canonical : bool;
}
type constructor_expr = (Names.lident * Constrexpr.constr_expr) with_coercion
type constructor_list_or_record_decl_expr =
| Constructors of constructor_expr list
| RecordDecl of Names.lident option * (local_decl_expr * record_field_attr) list * Names.lident option
type inductive_params_expr = Constrexpr.local_binder_expr list * Constrexpr.local_binder_expr list option

If the option is nonempty the "|" marker was used

type inductive_expr = Constrexpr.cumul_ident_decl with_coercion * inductive_params_expr * Constrexpr.constr_expr option * constructor_list_or_record_decl_expr
type one_inductive_expr = Names.lident * inductive_params_expr * Constrexpr.constr_expr option * constructor_expr list
type typeclass_constraint = Constrexpr.name_decl * Glob_term.binding_kind * Constrexpr.constr_expr
and typeclass_context = typeclass_constraint list
type proof_expr = Constrexpr.ident_decl * (Constrexpr.local_binder_expr list * Constrexpr.constr_expr)
type opacity_flag =
| Opaque
| Transparent
type proof_end =
| Admitted
| Proved of opacity_flag * Names.lident option
type scheme_type =
| SchemeInduction
| SchemeMinimality
| SchemeElimination
| SchemeCase
type equality_scheme_type =
| SchemeBooleanEquality
| SchemeEquality
type scheme = {
sch_type : scheme_type;
sch_qualid : Libnames.qualid Constrexpr.or_by_notation;
sch_sort : Sorts.family;
}
type 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
type register_kind =
| RegisterInline
| RegisterCoqlib of Libnames.qualid
Types concerning the module layer
type module_ast_inl = Constrexpr.module_ast * Declaremods.inline
type module_binder = export_with_cats option * Names.lident list * module_ast_inl
The type of vernacular expressions
type vernac_one_argument_status = {
name : Names.Name.t;
recarg_like : bool;
notation_scope : string CAst.t option;
implicit_status : Glob_term.binding_kind;
}
type vernac_argument_status =
| VolatileArg
| BidiArg
| RealArg of vernac_one_argument_status
type arguments_modifier = [
| `Assert
| `ClearBidiHint
| `ClearImplicits
| `ClearScopes
| `DefaultImplicits
| `ExtraScopes
| `ReductionDontExposeCase
| `ReductionNeverUnfold
| `Rename
]
type extend_name = string * int
type discharge =
| DoDischarge
| NoDischarge
type hint_info_expr = Constrexpr.constr_pattern_expr Typeclasses.hint_info_gen
type reference_or_constr =
| HintsReference of Libnames.qualid
| HintsConstr of Constrexpr.constr_expr
type 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
type nonrec vernac_expr =
| VernacLoad of verbose_flag * string
| VernacReservedNotation of infix_flag * Names.lstring * syntax_modifier CAst.t list
| VernacOpenCloseScope of bool * scope_name
| VernacDeclareScope of scope_name
| VernacDelimiters of scope_name * string option
| VernacBindScope of scope_name * class_rawexpr list
| VernacNotation of infix_flag * Constrexpr.constr_expr * Names.lstring * syntax_modifier CAst.t list * scope_name option
| VernacNotationAddFormat of string * string * string
| VernacDeclareCustomEntry of string
| 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 * decl_notation 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
| VernacBeginSection of Names.lident
| VernacEndSegment of Names.lident
| VernacExtraDependency of Libnames.qualid * string * Names.Id.t option
| 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
| VernacCanonical of Libnames.qualid Constrexpr.or_by_notation
| VernacCoercion of Libnames.qualid Constrexpr.or_by_notation * (class_rawexpr * class_rawexpr) option
| VernacIdentityCoercion of Names.lident * class_rawexpr * class_rawexpr
| 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
| 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
| VernacAddLoadPath of {
implicit : bool;
physical_path : CUnix.physical_path;
logical_path : Names.DirPath.t;
}
| VernacRemoveLoadPath of string
| VernacAddMLPath of string
| VernacDeclareMLModule of string list
| VernacChdir of string option
| 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
| VernacSetOption of bool * Goptions.option_name * option_setting
| VernacAddOption of Goptions.option_name * Goptions.table_value list
| VernacRemoveOption of Goptions.option_name * Goptions.table_value 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
| VernacProof of Genarg.raw_generic_argument option * section_subset_expr option
| VernacProofMode of string
| VernacExtend of extend_name * Genarg.raw_generic_argument list
type control_flag =
| ControlTime of bool
| ControlRedirect of string
| ControlTimeout of int
| ControlFail
| ControlSucceed
type vernac_control_r = {
control : control_flag list;
attrs : Attributes.vernac_flags;
expr : vernac_expr;
}
and vernac_control = vernac_control_r CAst.t