package coq

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

Module TactypesSource

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

Sourcetype 'constr intro_pattern_expr =
  1. | IntroForthcoming of bool
  2. | IntroNaming of Namegen.intro_pattern_naming_expr
  3. | IntroAction of 'constr intro_pattern_action_expr
Sourceand '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
Sourceand '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

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