Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Source file vernacexpr.ml
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501(************************************************************************)(* * The Coq Proof Assistant / The Coq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \VV/ **************************************************************)(* // * This file is distributed under the terms of the *)(* * GNU Lesser General Public License Version 2.1 *)(* * (see LICENSE file for the text of the license) *)(************************************************************************)openNamesopenConstrexpropenLibnames(** Vernac expressions, produced by the parser *)typeclass_rawexpr=FunClass|SortClass|RefClassofqualidor_by_notationtypegoal_identifier=stringtypescope_name=stringtypegoal_reference=|OpenSubgoals|NthGoalofint|GoalIdofId.ttypeprintable=|PrintTypingFlags|PrintTables|PrintFullContext|PrintSectionContextofqualid|PrintInspectofint|PrintGrammarofstringlist|PrintCustomGrammarofstring|PrintKeywords|PrintLoadPathofDirPath.toption|PrintLibraries|PrintModuleofqualid|PrintModuleTypeofqualid|PrintNamespaceofDirPath.t|PrintMLLoadPath|PrintMLModules|PrintDebugGC|PrintNameofqualidor_by_notation*UnivNames.univ_name_listoption|PrintGraph|PrintClasses|PrintTypeclasses|PrintInstancesofqualidor_by_notation|PrintCoercions|PrintCoercionPathsofclass_rawexpr*class_rawexpr|PrintCanonicalConversionsofqualidor_by_notationlist|PrintUniversesofbool*qualidlistoption*stringoption|PrintHintofqualidor_by_notation|PrintHintGoal|PrintHintDbNameofstring|PrintHintDb|PrintScopes|PrintScopeofstring|PrintVisibilityofstringoption|PrintAboutofqualidor_by_notation*UnivNames.univ_name_listoption*Goal_select.toption|PrintImplicitofqualidor_by_notation|PrintAssumptionsofbool*bool*qualidor_by_notation|PrintStrategyofqualidor_by_notationoption|PrintRegistered|PrintNotationofConstrexpr.notation_entry*stringtypeglob_search_where=InHyp|InConcl|Anywheretypesearch_item=|SearchSubPatternof(glob_search_where*bool)*constr_pattern_expr|SearchStringof(glob_search_where*bool)*string*scope_nameoption|SearchKindofDecls.logical_kindtypesearch_request=|SearchLiteralofsearch_item|SearchDisjConjof(bool*search_request)listlisttypesearchable=|SearchPatternofconstr_pattern_expr|SearchRewriteofconstr_pattern_expr|Searchof(bool*search_request)listtypelocatable=|LocateAnyofqualidor_by_notation|LocateTermofqualidor_by_notation|LocateLibraryofqualid|LocateModuleofqualid|LocateOtherofstring*qualid|LocateFileofstringtypeshowable=|ShowGoalofgoal_reference|ShowProof|ShowExistentials|ShowUniverses|ShowProofNames|ShowIntrosofbool|ShowMatchofqualidtypecomment=|CommentConstrofconstr_expr|CommentStringofstring|CommentIntofinttypesearch_restriction=|SearchInsideofqualidlist|SearchOutsideofqualidlisttypeverbose_flag=bool(* true = Verbose; false = Silent *)typecoercion_flag=AddCoercion|NoCoercion(* Remove BackInstanceWarning at end of deprecation phase
(this is just to print a warning when :> is used instead of ::
to declare instances in classes) *)typeinstance_flag=BackInstance|BackInstanceWarning|NoInstancetypeexport_flag=Lib.export_flag=Export|Importtypeimport_categories={negative:bool;import_cats:stringCAst.tlist;}typeexport_with_cats=export_flag*import_categoriesoptiontypeinfix_flag=bool(* true = Infix; false = Notation *)typeone_import_filter_name=qualid*bool(* import inductive components *)typeimport_filter_expr=|ImportAll|ImportNamesofone_import_filter_namelisttypelocality_flag=bool(* true = Local *)typeoption_setting=|OptionUnset|OptionSetTrue|OptionSetIntofint|OptionSetStringofstring(** Identifier and optional list of bound universes and constraints. *)typedefinition_expr=|ProveBodyoflocal_binder_exprlist*constr_expr|DefineBodyoflocal_binder_exprlist*Genredexpr.raw_red_exproption*constr_expr*constr_exproptiontypenotation_format=|TextFormatoflstringtypesyntax_modifier=|SetItemLevelofstringlist*Notation_term.constr_as_binder_kindoption*Extend.production_level|SetItemScopeofstringlist*scope_name|SetLevelofint|SetCustomEntryofstring*intoption|SetAssocofGramlib.Gramext.g_assoc|SetEntryTypeofstring*Extend.simple_constr_prod_entry_key|SetOnlyParsing|SetOnlyPrinting|SetFormatofnotation_formattypenotation_enable_modifier=|EnableNotationEntryofnotation_entryCAst.t|EnableNotationOnlyofNotationextern.notation_use|EnableNotationAlltypedecl_notation={decl_ntn_string:lstring;decl_ntn_interp:constr_expr;decl_ntn_scope:scope_nameoption;decl_ntn_modifiers:syntax_modifierCAst.tlist}type'afix_expr_gen={fname:lident;univs:universe_decl_exproption;rec_order:'a;binders:local_binder_exprlist;rtype:constr_expr;body_def:constr_exproption;notations:decl_notationlist}typefixpoint_expr=recursion_order_exproptionfix_expr_gentypecofixpoint_expr=unitfix_expr_gentypelocal_decl_expr=|AssumExproflname*local_binder_exprlist*constr_expr|DefExproflname*local_binder_exprlist*constr_expr*constr_exproptiontypeinductive_kind=Inductive_kw|CoInductive|Variant|Record|Structure|Classofbool(* true = definitional, false = inductive *)typesimple_binder=lidentlist*constr_exprtypeclass_binder=lident*constr_exprlisttype'awith_coercion=coercion_flag*'atype'awith_coercion_instance=(coercion_flag*instance_flag)*'a(* Attributes of a record field declaration *)typerecord_field_attr={rf_coercion:coercion_flag;(* the projection is an implicit coercion *)rf_reversible:booloption;(* coercion is reversible, if relevant *)rf_instance:instance_flag;(* the projection is an instance *)rf_priority:intoption;(* priority of the instance, if relevant *)rf_locality:Goptions.option_locality;(* locality of coercion and instance *)rf_notation:decl_notationlist;rf_canonical:bool;(* use this projection in the search for canonical instances *)}typeconstructor_expr=(lident*constr_expr)with_coercion_instancetypeconstructor_list_or_record_decl_expr=|Constructorsofconstructor_exprlist|RecordDecloflidentoption*(local_decl_expr*record_field_attr)list*lidentoptiontypeinductive_params_expr=local_binder_exprlist*local_binder_exprlistoption(** If the option is nonempty the "|" marker was used *)typeinductive_expr=cumul_ident_declwith_coercion*inductive_params_expr*constr_exproption*constructor_list_or_record_decl_exprtypeone_inductive_expr=lident*inductive_params_expr*constr_exproption*constructor_exprlisttypetypeclass_constraint=name_decl*Glob_term.binding_kind*constr_exprandtypeclass_context=typeclass_constraintlisttypeproof_expr=ident_decl*(local_binder_exprlist*constr_expr)typeopacity_flag=Opaque|Transparenttypeproof_end=|Admitted(* name in `Save ident` when closing goal *)|Provedofopacity_flag*lidentoptiontypescheme_type=|SchemeInduction|SchemeMinimality|SchemeElimination|SchemeCasetypeequality_scheme_type=|SchemeBooleanEquality|SchemeEquality(* The data of a Scheme decleration *)typescheme={sch_type:scheme_type;sch_qualid:Libnames.qualidConstrexpr.or_by_notation;sch_sort:Sorts.family;}typesection_subset_expr=|SsEmpty|SsType|SsSingloflident|SsComplofsection_subset_expr|SsUnionofsection_subset_expr*section_subset_expr|SsSubstrofsection_subset_expr*section_subset_expr|SsFwdCloseofsection_subset_expr(** Extension identifiers for the VERNAC EXTEND mechanism.
{b ("Extraction", 0} indicates {b Extraction {i qualid}} command.
{b ("Extraction", 1} indicates {b Recursive Extraction {i qualid}} command.
{b ("Extraction", 2)} indicates {b Extraction "{i filename}" {i qualid{_ 1}} ... {i qualid{_ n}}} command.
{b ("ExtractionLibrary", 0)} indicates {b Extraction Library {i ident}} command.
{b ("RecursiveExtractionLibrary", 0)} indicates {b Recursive Extraction Library {i ident}} command.
{b ("SeparateExtraction", 0)} indicates {b Separate Extraction {i qualid{_ 1}} ... {i qualid{_ n}}} command.
{b ("ExtractionLanguage", 0)} indicates {b Extraction Language Ocaml} or {b Extraction Language Haskell} or {b Extraction Language Scheme} or {b Extraction Language JSON} commands.
{b ("ExtractionImplicit", 0)} indicates {b Extraction Implicit {i qualid} \[ {i ident{_1}} ... {i ident{_n} } \] } command.
{b ("ExtractionConstant", 0)} indicates {b Extract Constant {i qualid} => {i string}} command.
{b ("ExtractionInlinedConstant", 0)} indicates {b Extract Inlined Constant {i qualid} => {i string}} command.
{b ("ExtractionInductive", 0)} indicates {b Extract Inductive {i qualid} => {i string} [ {i string} ... {string} ] {i optstring}} command.
{b ("ExtractionBlacklist", 0)} indicates {b Extraction Blacklist {i ident{_1}} ... {i ident{_n}}} command.
*)(* This type allows registering the inlining of constants in native compiler.
It will be extended with primitive inductive types and operators *)typeregister_kind=|RegisterInline|RegisterCoqlibofqualid(** {6 Types concerning the module layer} *)typemodule_ast_inl=module_ast*Declaremods.inlinetypemodule_binder=export_with_catsoption*lidentlist*module_ast_inl(** {6 The type of vernacular expressions} *)typevernac_one_argument_status={name:Name.t;recarg_like:bool;notation_scope:stringCAst.tlist;implicit_status:Glob_term.binding_kind;}typevernac_argument_status=|VolatileArg|BidiArg|RealArgofvernac_one_argument_statustypearguments_modifier=[`Assert|`ClearBidiHint|`ClearImplicits|`ClearScopes|`DefaultImplicits|`ExtraScopes|`ReductionDontExposeCase|`ReductionNeverUnfold|`Rename]typeextend_name=(* Name of the vernac entry where the tactic is defined, typically found
after the VERNAC EXTEND statement in the source. *)string*(* Index of the extension in the VERNAC EXTEND statement. Each parsing branch
is given an offset, starting from zero. *)inttypedischarge=DoDischarge|NoDischargetypehint_info_expr=Constrexpr.constr_pattern_exprTypeclasses.hint_info_gentypereference_or_constr=|HintsReferenceofLibnames.qualid|HintsConstrofConstrexpr.constr_exprtypehints_expr=|HintsResolveof(hint_info_expr*bool*reference_or_constr)list|HintsResolveIFFofbool*Libnames.qualidlist*intoption|HintsImmediateofreference_or_constrlist|HintsUnfoldofLibnames.qualidlist|HintsTransparencyofLibnames.qualidHints.hints_transparency_target*bool|HintsModeofLibnames.qualid*Hints.hint_modelist|HintsConstructorsofLibnames.qualidlist|HintsExternofint*Constrexpr.constr_exproption*Genarg.raw_generic_argumenttypenonrecvernac_expr=|VernacLoadofverbose_flag*string(* Syntax *)|VernacReservedNotationofinfix_flag*(lstring*syntax_modifierCAst.tlist)|VernacOpenCloseScopeofbool*scope_name|VernacDeclareScopeofscope_name|VernacDelimitersofscope_name*stringoption|VernacBindScopeofscope_name*class_rawexprlist|VernacNotationofinfix_flag*constr_expr*(lstring*syntax_modifierCAst.tlist)*scope_nameoption|VernacDeclareCustomEntryofstring|VernacEnableNotationofbool*(string,Id.tlist*qualid)Util.unionoption*constr_exproption*notation_enable_modifierlist*notation_with_optional_scopeoption(* Gallina *)|VernacDefinitionof(discharge*Decls.definition_object_kind)*name_decl*definition_expr|VernacStartTheoremProofofDecls.theorem_kind*proof_exprlist|VernacEndProofofproof_end|VernacExactProofofconstr_expr|VernacAssumptionof(discharge*Decls.assumption_object_kind)*Declaremods.inline*(ident_decllist*constr_expr)with_coercionlist|VernacInductiveofinductive_kind*(inductive_expr*decl_notationlist)list|VernacFixpointofdischarge*fixpoint_exprlist|VernacCoFixpointofdischarge*cofixpoint_exprlist|VernacSchemeof(lidentoption*scheme)list|VernacSchemeEqualityofequality_scheme_type*Libnames.qualidConstrexpr.or_by_notation|VernacCombinedSchemeoflident*lidentlist|VernacUniverseoflidentlist|VernacConstraintofuniv_constraint_exprlist(* Gallina extensions *)|VernacBeginSectionoflident|VernacEndSegmentoflident|VernacExtraDependencyofqualid*string*Id.toption|VernacRequireofqualidoption*export_with_catsoption*(qualid*import_filter_expr)list|VernacImportofexport_with_cats*(qualid*import_filter_expr)list|VernacCanonicalofqualidor_by_notation|VernacCoercionofqualidor_by_notation*(class_rawexpr*class_rawexpr)option|VernacIdentityCoercionoflident*class_rawexpr*class_rawexpr|VernacNameSectionHypSetoflident*section_subset_expr(* Type classes *)|VernacInstanceofname_decl*(* name *)local_binder_exprlist*(* binders *)constr_expr*(* type *)(bool*constr_expr)option*(* body (bool=true when using {}) *)hint_info_expr|VernacDeclareInstanceofident_decl*(* name *)local_binder_exprlist*(* binders *)constr_expr*(* type *)hint_info_expr|VernacContextoflocal_binder_exprlist|VernacExistingInstanceof(qualid*hint_info_expr)list(* instances names, priorities and patterns *)|VernacExistingClassofqualid(* inductive or definition name *)(* Modules and Module Types *)|VernacDeclareModuleofexport_with_catsoption*lident*module_binderlist*module_ast_inl|VernacDefineModuleofexport_with_catsoption*lident*module_binderlist*module_ast_inlDeclaremods.module_signature*module_ast_inllist|VernacDeclareModuleTypeoflident*module_binderlist*module_ast_inllist*module_ast_inllist|VernacIncludeofmodule_ast_inllist(* Auxiliary file and library management *)|VernacAddLoadPathof{implicit:bool;physical_path:CUnix.physical_path;logical_path:DirPath.t}|VernacRemoveLoadPathofstring|VernacAddMLPathofstring|VernacDeclareMLModuleofstringlist|VernacChdirofstringoption(* Resetting *)|VernacResetNameoflident|VernacResetInitial|VernacBackofint(* Commands *)|VernacCreateHintDbofstring*bool|VernacRemoveHintsofstringlist*qualidlist|VernacHintsofstringlist*hints_expr|VernacSyntacticDefinitionoflident*(Id.tlist*constr_expr)*syntax_modifierCAst.tlist|VernacArgumentsofqualidor_by_notation*vernac_argument_statuslist(* Main arguments status list *)*(Name.t*Glob_term.binding_kind)listlist(* Extra implicit status lists *)*arguments_modifierlist|VernacReserveofsimple_binderlist|VernacGeneralizableof(lidentlist)option|VernacSetOpacityof(Conv_oracle.level*qualidor_by_notationlist)|VernacSetStrategyof(Conv_oracle.level*qualidor_by_notationlist)list|VernacSetOptionofbool(* Export modifier? *)*Goptions.option_name*option_setting|VernacAddOptionofGoptions.option_name*Goptions.table_valuelist|VernacRemoveOptionofGoptions.option_name*Goptions.table_valuelist|VernacMemOptionofGoptions.option_name*Goptions.table_valuelist|VernacPrintOptionofGoptions.option_name|VernacCheckMayEvalofGenredexpr.raw_red_exproption*Goal_select.toption*constr_expr|VernacGlobalCheckofconstr_expr|VernacDeclareReductionofstring*Genredexpr.raw_red_expr|VernacPrintofprintable|VernacSearchofsearchable*Goal_select.toption*search_restriction|VernacLocateoflocatable|VernacRegisterofqualid*register_kind|VernacPrimitiveofident_decl*CPrimitives.op_or_type*constr_exproption|VernacCommentsofcommentlist(* Proof management *)|VernacAbort|VernacAbortAll|VernacRestart|VernacUndoofint|VernacUndoToofint|VernacFocusofintoption|VernacUnfocus|VernacUnfocused|VernacBulletofProof_bullet.t|VernacSubproofofGoal_select.toption|VernacEndSubproof|VernacShowofshowable|VernacCheckGuard|VernacProofofGenarg.raw_generic_argumentoption*section_subset_exproption|VernacProofModeofstring(* For extension *)|VernacExtendofextend_name*Genarg.raw_generic_argumentlisttypecontrol_flag=|ControlTimeofbool(* boolean is true when the `-time` batch-mode command line flag was set.
the flag is used to print differently in `-time` vs `Time foo` *)|ControlRedirectofstring|ControlTimeoutofint|ControlFail|ControlSucceedtypevernac_control_r={control:control_flaglist;attrs:Attributes.vernac_flags;expr:vernac_expr}andvernac_control=vernac_control_rCAst.t