package coq

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

Tactic-related types that are not totally Ltac specific and still used in lower API. It's not clear whether this is a temporary API or if this is meant to stay.

Introduction patterns

type 'constr intro_pattern_expr =
  1. | IntroForthcoming of bool
  2. | IntroNaming of Namegen.intro_pattern_naming_expr
  3. | IntroAction of 'constr intro_pattern_action_expr
and 'constr intro_pattern_action_expr =
  1. | IntroWildcard
  2. | IntroOrAndPattern of 'constr or_and_intro_pattern_expr
  3. | IntroInjection of 'constr intro_pattern_expr CAst.t list
  4. | IntroApplyOn of 'constr CAst.t * 'constr intro_pattern_expr CAst.t
  5. | IntroRewrite of bool
and 'constr or_and_intro_pattern_expr =
  1. | IntroOrPattern of 'constr intro_pattern_expr CAst.t list list
  2. | IntroAndPattern of 'constr intro_pattern_expr CAst.t list

Bindings

type quantified_hypothesis =
  1. | AnonHyp of int
  2. | NamedHyp of Names.Id.t
type 'a explicit_bindings = (quantified_hypothesis * 'a) CAst.t list
type 'a bindings =
  1. | ImplicitBindings of 'a list
  2. | ExplicitBindings of 'a explicit_bindings
  3. | NoBindings
type 'a with_bindings = 'a * 'a bindings
type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a
type delayed_open_constr = EConstr.constr delayed_open
type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open
type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list
type intro_pattern_naming = Namegen.intro_pattern_naming_expr 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