package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct