package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.19.0.tar.gz
md5=64b49dbc3205477bd7517642c0b9cbb6
sha512=02fb5b4fb575af79e092492cbec6dc0d15a1d74a07f827f657a72d4e6066532630e5a6d15be4acdb73314bd40b9a321f9ea0584e0ccfe51fd3a56353bd30db9b

doc/ltac2_plugin/Ltac2_plugin/Tac2qexpr/index.html

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