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
| PrintModules
| 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
| 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
type search_about_item =
| SearchSubPattern of Constrexpr.constr_pattern_expr
| SearchString of string * scope_name option
type searchable =
| SearchPattern of Constrexpr.constr_pattern_expr
| SearchRewrite of Constrexpr.constr_pattern_expr
| SearchHead of Constrexpr.constr_pattern_expr
| SearchAbout of (bool * search_about_item) list
| Search of (bool * search_about_item) 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 rec_flag = bool
type verbose_flag = bool
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_setting =
| OptionUnset
| OptionSetTrue
| OptionSetInt of int
| OptionSetString of string
type option_ref_value =
| StringRefValue of string
| QualidRefValue of Libnames.qualid
type sort_expr = Sorts.family
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 decl_notation = Names.lstring * Constrexpr.constr_expr * scope_name option
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.constr_expr
| DefExpr of Names.lname * 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_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
type inductive_expr = Constrexpr.ident_decl with_coercion * Constrexpr.local_binder_expr list * Constrexpr.constr_expr option * inductive_kind * constructor_list_or_record_decl_expr
type one_inductive_expr = Names.lident * Constrexpr.local_binder_expr list * 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 syntax_modifier =
| SetItemLevel of string list * Notation_term.constr_as_binder_kind option * Extend.production_level option
| 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
| SetCompatVersion of Flags.compat_version
| SetFormat of string * Names.lstring
type proof_end =
| Admitted
| Proved of Proof_global.opacity_flag * Names.lident option
type scheme =
| InductionScheme of bool * Libnames.qualid Constrexpr.or_by_notation * sort_expr
| CaseScheme of bool * Libnames.qualid Constrexpr.or_by_notation * sort_expr
| EqualityScheme of Libnames.qualid Constrexpr.or_by_notation
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 = bool option * Names.lident list * module_ast_inl
type vernac_cumulative =
| VernacCumulative
| VernacNonCumulative

Some b if locally enabled/disabled according to b, None if we should use the global flag.

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 : Impargs.implicit_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 nonrec vernac_expr =
| VernacLoad of verbose_flag * string
| VernacSyntaxExtension of bool * Names.lstring * syntax_modifier list
| VernacOpenCloseScope of bool * scope_name
| VernacDeclareScope of scope_name
| VernacDelimiters of scope_name * string option
| VernacBindScope of scope_name * class_rawexpr list
| VernacInfix of Names.lstring * syntax_modifier list * Constrexpr.constr_expr * scope_name option
| VernacNotation of Constrexpr.constr_expr * Names.lstring * syntax_modifier 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 vernac_cumulative option * bool * inductive_flag * (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
| VernacCombinedScheme of Names.lident * Names.lident list
| VernacUniverse of Names.lident list
| VernacConstraint of Glob_term.glob_constraint list
| VernacBeginSection of Names.lident
| VernacEndSegment of Names.lident
| VernacRequire of Libnames.qualid option * export_flag option * Libnames.qualid list
| VernacImport of export_flag * Libnames.qualid list
| VernacCanonical of Libnames.qualid Constrexpr.or_by_notation
| VernacCoercion of Libnames.qualid Constrexpr.or_by_notation * class_rawexpr * class_rawexpr
| 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 * Hints.hint_info_expr
| VernacDeclareInstance of Constrexpr.ident_decl * Constrexpr.local_binder_expr list * Constrexpr.constr_expr * Hints.hint_info_expr
| VernacContext of Constrexpr.local_binder_expr list
| VernacExistingInstance of (Libnames.qualid * Hints.hint_info_expr) list
| VernacExistingClass of Libnames.qualid
| VernacDeclareModule of bool option * Names.lident * module_binder list * module_ast_inl
| VernacDefineModule of bool 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
| VernacSolveExistential of int * Constrexpr.constr_expr
| VernacAddLoadPath of rec_flag * string * Names.DirPath.t option
| VernacRemoveLoadPath of string
| VernacAddMLPath of rec_flag * string
| VernacDeclareMLModule of string list
| VernacChdir of string option
| VernacWriteState of string
| VernacRestoreState of string
| VernacResetName of Names.lident
| VernacResetInitial
| VernacBack of int
| VernacCreateHintDb of string * bool
| VernacRemoveHints of string list * Libnames.qualid list
| VernacHints of string list * Hints.hints_expr
| VernacSyntacticDefinition of Names.lident * Names.Id.t list * Constrexpr.constr_expr * onlyparsing_flag
| VernacArguments of Libnames.qualid Constrexpr.or_by_notation * vernac_argument_status list * (Names.Name.t * Impargs.implicit_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 export_flag * Goptions.option_name * option_setting
| VernacAddOption of Goptions.option_name * option_ref_value list
| VernacRemoveOption of Goptions.option_name * option_ref_value list
| VernacMemOption of Goptions.option_name * option_ref_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 Names.lident * CPrimitives.op_or_type * Constrexpr.constr_expr option
| VernacComments of comment list
| VernacAbort of Names.lident option
| 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
type vernac_control_r = {
control : control_flag list;
attrs : Attributes.vernac_flags;
expr : vernac_expr;
}
and vernac_control = vernac_control_r CAst.t