(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* red | FBeta :: lf -> add_flag { red with rBeta = true } lf | FIota :: lf -> add_flag { red with rIota = true } lf | FZeta :: lf -> add_flag { red with rZeta = true } lf | FConst l :: lf -> if red.rDelta then error "Cannot set both constants to unfold and constants not to unfold"; add_flag { red with rConst = list_union red.rConst l } lf | FDeltaBut l :: lf -> if red.rConst <> [] & not red.rDelta then error "Cannot set both constants to unfold and constants not to unfold"; add_flag { red with rConst = list_union red.rConst l; rDelta = true } lf in add_flag {rBeta = false; rIota = false; rZeta = false; rDelta = false; rConst = []} type 'a raw_hyp_location = 'a with_occurrences * Termops.hyp_location_flag type 'id move_location = | MoveAfter of 'id | MoveBefore of 'id | MoveToEnd of bool let no_move = MoveToEnd true open Pp let pr_move_location pr_id = function | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id | MoveToEnd toleft -> str (if toleft then " at bottom" else " at top") type 'a induction_arg = | ElimOnConstr of 'a | ElimOnIdent of identifier located | ElimOnAnonHyp of int type inversion_kind = | SimpleInversion | FullInversion | FullInversionClear type ('c,'id) inversion_strength = | NonDepInversion of inversion_kind * 'id list * intro_pattern_expr located option | DepInversion of inversion_kind * 'c option * intro_pattern_expr located option | InversionUsing of 'c * 'id list type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b type 'id message_token = | MsgString of string | MsgInt of int | MsgIdent of 'id (* onhyps: [None] means *on every hypothesis* [Some l] means on hypothesis belonging to l *) type 'id gclause = { onhyps : 'id raw_hyp_location list option; concl_occs : occurrences_expr } let nowhere = {onhyps=Some[]; concl_occs=no_occurrences_expr} type 'constr induction_clause = ('constr with_bindings induction_arg list * 'constr with_bindings option * (intro_pattern_expr located option * intro_pattern_expr located option)) type ('constr,'id) induction_clause_list = 'constr induction_clause list * 'id gclause option type multi = | Precisely of int | UpTo of int | RepeatStar | RepeatPlus (* Type of patterns *) type 'a match_pattern = | Term of 'a | Subterm of bool * identifier option * 'a (* Type of hypotheses for a Match Context rule *) type 'a match_context_hyps = | Hyp of name located * 'a match_pattern | Def of name located * 'a match_pattern * 'a match_pattern (* Type of a Match rule for Match Context and Match *) type ('a,'t) match_rule = | Pat of 'a match_context_hyps list * 'a match_pattern * 't | All of 't type ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_atomic_tactic_expr = (* Basic tactics *) | TacIntroPattern of intro_pattern_expr located list | TacIntrosUntil of quantified_hypothesis | TacIntroMove of identifier option * 'id move_location | TacAssumption | TacExact of 'constr | TacExactNoCheck of 'constr | TacVmCastNoCheck of 'constr | TacApply of advanced_flag * evars_flag * 'constr with_bindings list * ('id * intro_pattern_expr located option) option | TacElim of evars_flag * 'constr with_bindings * 'constr with_bindings option | TacElimType of 'constr | TacCase of evars_flag * 'constr with_bindings | TacCaseType of 'constr | TacFix of identifier option * int | TacMutualFix of hidden_flag * identifier * int * (identifier * int * 'constr) list | TacCofix of identifier option | TacMutualCofix of hidden_flag * identifier * (identifier * 'constr) list | TacCut of 'constr | TacAssert of 'tac option * intro_pattern_expr located option * 'constr | TacGeneralize of ('constr with_occurrences * name) list | TacGeneralizeDep of 'constr | TacLetTac of name * 'constr * 'id gclause * letin_flag (* Derived basic tactics *) | TacSimpleInductionDestruct of rec_flag * quantified_hypothesis | TacInductionDestruct of rec_flag * evars_flag * ('constr,'id) induction_clause_list | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis | TacDecomposeAnd of 'constr | TacDecomposeOr of 'constr | TacDecompose of 'ind list * 'constr | TacSpecialize of int option * 'constr with_bindings | TacLApply of 'constr (* Automation tactics *) | TacTrivial of debug * 'constr list * string list option | TacAuto of debug * int or_var option * 'constr list * string list option | TacDAuto of debug * int or_var option * int option * 'constr list (* Context management *) | TacClear of bool * 'id list | TacClearBody of 'id list | TacMove of bool * 'id * 'id move_location | TacRename of ('id *'id) list | TacRevert of 'id list (* Constructors *) | TacLeft of evars_flag * 'constr bindings | TacRight of evars_flag * 'constr bindings | TacSplit of evars_flag * split_flag * 'constr bindings list | TacAnyConstructor of evars_flag * 'tac option | TacConstructor of evars_flag * int or_var * 'constr bindings (* Conversion *) | TacReduce of ('constr,'cst,'pat) red_expr_gen * 'id gclause | TacChange of 'pat option * 'constr * 'id gclause (* Equivalence relations *) | TacReflexivity | TacSymmetry of 'id gclause | TacTransitivity of 'constr option (* Equality and inversion *) | TacRewrite of evars_flag * (bool * multi * 'constr with_bindings) list * 'id gclause * 'tac option | TacInversion of ('constr,'id) inversion_strength * quantified_hypothesis (* For ML extensions *) | TacExtend of loc * string * 'lev generic_argument list (* For syntax extensions *) | TacAlias of loc * string * (identifier * 'lev generic_argument) list * (dir_path * glob_tactic_expr) and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr = | TacAtom of loc * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_atomic_tactic_expr | TacThen of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr array * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr array | TacThens of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr list | TacFirst of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr list | TacComplete of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr | TacSolve of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr list | TacTry of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr | TacOrelse of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr | TacDo of int or_var * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr | TacTimeout of int or_var * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr | TacRepeat of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr | TacProgress of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr | TacAbstract of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr * identifier option | TacId of 'id message_token list | TacFail of int or_var * 'id message_token list | TacInfo of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr | TacLetIn of rec_flag * (identifier located * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg) list * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr | TacMatch of lazy_flag * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr) match_rule list | TacMatchGoal of lazy_flag * direction_flag * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr) match_rule list | TacFun of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_fun_ast | TacArg of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg located and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_fun_ast = identifier option list * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr (* These are the possible arguments of a tactic definition *) and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg = | TacDynamic of loc * Dyn.t | TacVoid | MetaIdArg of loc * bool * string | ConstrMayEval of ('constr,'cst,'pat) may_eval | IntroPattern of intro_pattern_expr located | Reference of 'ref | Integer of int | TacCall of loc * 'ref * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg list | TacExternal of loc * string * string * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg list | TacFreshId of string or_var list | Tacexp of 'tac (* Globalized tactics *) and glob_tactic_expr = (glob_constr_and_expr, glob_constr_and_expr * constr_pattern, evaluable_global_reference and_short_name or_var, inductive or_var, ltac_constant located or_var, identifier located, glob_tactic_expr, glevel) gen_tactic_expr type raw_tactic_expr = (constr_expr, constr_pattern_expr, reference or_by_notation, reference or_by_notation, reference, identifier located or_metaid, raw_tactic_expr, rlevel) gen_tactic_expr type raw_atomic_tactic_expr = (constr_expr, (* constr *) constr_pattern_expr, (* pattern *) reference or_by_notation, (* evaluable reference *) reference or_by_notation, (* inductive *) reference, (* ltac reference *) identifier located or_metaid, (* identifier *) raw_tactic_expr, rlevel) gen_atomic_tactic_expr type raw_tactic_arg = (constr_expr, constr_pattern_expr, reference or_by_notation, reference or_by_notation, reference, identifier located or_metaid, raw_tactic_expr, rlevel) gen_tactic_arg type raw_generic_argument = rlevel generic_argument type raw_red_expr = (constr_expr, reference or_by_notation, constr_expr) red_expr_gen type glob_atomic_tactic_expr = (glob_constr_and_expr, glob_constr_and_expr * constr_pattern, evaluable_global_reference and_short_name or_var, inductive or_var, ltac_constant located or_var, identifier located, glob_tactic_expr, glevel) gen_atomic_tactic_expr type glob_tactic_arg = (glob_constr_and_expr, glob_constr_and_expr * constr_pattern, evaluable_global_reference and_short_name or_var, inductive or_var, ltac_constant located or_var, identifier located, glob_tactic_expr, glevel) gen_tactic_arg type glob_generic_argument = glevel generic_argument type glob_red_expr = (glob_constr_and_expr, evaluable_global_reference or_var, constr_pattern) red_expr_gen type typed_generic_argument = tlevel generic_argument type 'a raw_abstract_argument_type = ('a,rlevel) abstract_argument_type type 'a glob_abstract_argument_type = ('a,glevel) abstract_argument_type type 'a typed_abstract_argument_type = ('a,tlevel) abstract_argument_type type 'a declaration_hook = locality -> global_reference -> 'a