package coq

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

Redefinition of Ltac1 data structures because of impedance mismatch

type evars_flag = bool
type advanced_flag = bool
type 'a thunk = (unit, 'a) Tac2ffi.fun1
type quantified_hypothesis = Tactypes.quantified_hypothesis =
  1. | AnonHyp of int
  2. | NamedHyp of Names.lident
type explicit_bindings = (quantified_hypothesis * EConstr.t) list
type bindings =
  1. | ImplicitBindings of EConstr.t list
  2. | ExplicitBindings of explicit_bindings
  3. | NoBindings
type constr_with_bindings = EConstr.constr * bindings
type core_destruction_arg =
  1. | ElimOnConstr of constr_with_bindings Proofview.tactic
  2. | ElimOnIdent of Names.Id.t
  3. | ElimOnAnonHyp of int
type destruction_arg = core_destruction_arg
type intro_pattern =
  1. | IntroForthcoming of bool
  2. | IntroNaming of intro_pattern_naming
  3. | IntroAction of intro_pattern_action
and intro_pattern_naming =
  1. | IntroIdentifier of Names.Id.t
  2. | IntroFresh of Names.Id.t
  3. | IntroAnonymous
and intro_pattern_action =
  1. | IntroWildcard
  2. | IntroOrAndPattern of or_and_intro_pattern
  3. | IntroInjection of intro_pattern list
  4. | IntroApplyOn of EConstr.t thunk * intro_pattern
  5. | IntroRewrite of bool
and or_and_intro_pattern =
  1. | IntroOrPattern of intro_pattern list list
  2. | IntroAndPattern of intro_pattern list
type occurrences =
  1. | AllOccurrences
  2. | AllOccurrencesBut of int list
  3. | NoOccurrences
  4. | OnlyOccurrences of int list
type hyp_location_flag = Locus.hyp_location_flag =
  1. | InHyp
  2. | InHypTypeOnly
  3. | InHypValueOnly
type hyp_location = Names.Id.t * occurrences * hyp_location_flag
type clause = {
  1. onhyps : hyp_location list option;
  2. concl_occs : occurrences;
}
type induction_clause = destruction_arg * intro_pattern_naming option * or_and_intro_pattern option * clause option
type multi = Equality.multi =
  1. | Precisely of int
  2. | UpTo of int
  3. | RepeatStar
  4. | RepeatPlus
type rewriting = bool option * multi * constr_with_bindings Proofview.tactic
type assertion =
  1. | AssertType of intro_pattern option * EConstr.constr * unit thunk option
  2. | AssertValue of Names.Id.t * EConstr.constr
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