Module Ltac2_plugin.Tac2qexpr

Quoted variants of Ltac syntactic categories. Contrarily to the former, they sometimes allow anti-quotations. Used for notation scopes.

type 'a or_anti =
| QExpr of 'a
| QAnti of Names.Id.t CAst.t
type reference_r =
| QReference of Libnames.qualid
| QHypothesis of Names.Id.t
type reference = reference_r CAst.t
type quantified_hypothesis =
| QAnonHyp of int CAst.t
| QNamedHyp of Names.Id.t CAst.t
type bindings_r =
| QImplicitBindings of Constrexpr.constr_expr list
| QExplicitBindings of (quantified_hypothesis CAst.t or_anti * Constrexpr.constr_expr) CAst.t list
| QNoBindings
type bindings = bindings_r CAst.t
type intro_pattern_r =
| QIntroForthcoming of bool
| QIntroNaming of intro_pattern_naming
| QIntroAction of intro_pattern_action
and intro_pattern_naming_r =
| QIntroIdentifier of Names.Id.t CAst.t or_anti
| QIntroFresh of Names.Id.t CAst.t or_anti
| QIntroAnonymous
and intro_pattern_action_r =
| QIntroWildcard
| QIntroOrAndPattern of or_and_intro_pattern
| QIntroInjection of intro_pattern list CAst.t
| QIntroApplyOn of Constrexpr.constr_expr * intro_pattern
| QIntroRewrite of bool
and or_and_intro_pattern_r =
| QIntroOrPattern of intro_pattern list CAst.t list
| QIntroAndPattern of intro_pattern list CAst.t
and intro_pattern = intro_pattern_r CAst.t
and intro_pattern_naming = intro_pattern_naming_r CAst.t
and intro_pattern_action = intro_pattern_action_r CAst.t
and or_and_intro_pattern = or_and_intro_pattern_r CAst.t
type occurrences_r =
| QAllOccurrences
| QAllOccurrencesBut of int CAst.t or_anti list
| QNoOccurrences
| QOnlyOccurrences of int CAst.t or_anti list
type occurrences = occurrences_r CAst.t
type clause_r = {
q_onhyps : hyp_location list option;
q_concl_occs : occurrences;
}
type clause = clause_r CAst.t
type constr_with_bindings = (Constrexpr.constr_expr * bindings) CAst.t
type destruction_arg_r =
| QElimOnConstr of constr_with_bindings
| QElimOnIdent of Names.Id.t CAst.t
| QElimOnAnonHyp of int CAst.t
type destruction_arg = destruction_arg_r CAst.t
type induction_clause_r = {
indcl_arg : destruction_arg;
indcl_eqn : intro_pattern_naming option;
indcl_as : or_and_intro_pattern option;
indcl_in : clause option;
}
type induction_clause = induction_clause_r CAst.t
type conversion_r =
| QConvert of Constrexpr.constr_expr
| QConvertWith of Constrexpr.constr_expr * Constrexpr.constr_expr
type conversion = conversion_r CAst.t
type multi_r =
| QPrecisely of int CAst.t
| QUpTo of int CAst.t
| QRepeatStar
| QRepeatPlus
type multi = multi_r CAst.t
type orientation = bool option CAst.t
type rewriting_r = {
rew_orient : orientation;
rew_repeat : multi;
rew_equatn : constr_with_bindings;
}
type rewriting = rewriting_r CAst.t
type dispatch_r = Tac2expr.raw_tacexpr option list * (Tac2expr.raw_tacexpr option * Tac2expr.raw_tacexpr option list) option
type dispatch = dispatch_r CAst.t
type red_flag_r =
| QBeta
| QIota
| QMatch
| QFix
| QCofix
| QZeta
| QConst of reference or_anti list CAst.t
| QDeltaBut of reference or_anti list CAst.t
| QHead
type red_flag = red_flag_r CAst.t
type strategy_flag = red_flag list CAst.t
type constr_match_pattern_r =
| QConstrMatchPattern of Constrexpr.constr_expr
| QConstrMatchContext of Names.Id.t option * Constrexpr.constr_expr
type constr_match_pattern = constr_match_pattern_r CAst.t
type constr_match_branch = (constr_match_pattern * Tac2expr.raw_tacexpr) CAst.t
type constr_matching = constr_match_branch list CAst.t
type goal_match_pattern_r = {
q_goal_match_concl : constr_match_pattern;
q_goal_match_hyps : (Names.lname * constr_match_pattern option * constr_match_pattern) list;
}
type goal_match_pattern = goal_match_pattern_r CAst.t
type goal_match_branch = (goal_match_pattern * Tac2expr.raw_tacexpr) CAst.t
type goal_matching = goal_match_branch list CAst.t
type hintdb_r =
| QHintAll
| QHintDbs of Names.Id.t CAst.t or_anti list
type hintdb = hintdb_r CAst.t
type move_location_r =
| QMoveAfter of Names.Id.t CAst.t or_anti
| QMoveBefore of Names.Id.t CAst.t or_anti
| QMoveFirst
| QMoveLast
type move_location = move_location_r CAst.t
type assertion_r =
| QAssertType of intro_pattern option * Constrexpr.constr_expr * Tac2expr.raw_tacexpr option
| QAssertValue of Names.Id.t CAst.t or_anti * Constrexpr.constr_expr
type assertion = assertion_r CAst.t