package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type patvar = Names.Id.t
type !'constr intro_pattern_expr =
  1. | IntroForthcoming of bool
  2. | IntroNaming of intro_pattern_naming_expr
  3. | IntroAction of 'constr intro_pattern_action_expr
and intro_pattern_naming_expr =
  1. | IntroIdentifier of Names.Id.t
  2. | IntroFresh of Names.Id.t
  3. | IntroAnonymous
and !'constr intro_pattern_action_expr =
  1. | IntroWildcard
  2. | IntroOrAndPattern of 'constr or_and_intro_pattern_expr
  3. | IntroInjection of 'constr intro_pattern_expr Loc.located list
  4. | IntroApplyOn of 'constr Loc.located * 'constr intro_pattern_expr Loc.located
  5. | IntroRewrite of bool
and !'constr or_and_intro_pattern_expr =
  1. | IntroOrPattern of 'constr intro_pattern_expr Loc.located list list
  2. | IntroAndPattern of 'constr intro_pattern_expr Loc.located list
type !'id move_location =
  1. | MoveAfter of 'id
  2. | MoveBefore of 'id
  3. | MoveFirst
  4. | MoveLast
type !'a glob_sort_gen =
  1. | GProp
  2. | GSet
  3. | GType of 'a
type sort_info = Names.Name.t Loc.located list
type level_info = Names.Name.t Loc.located option
type glob_sort = sort_info glob_sort_gen
type glob_level = level_info glob_sort_gen
type existential_key = Evar.t
type case_style = Term.case_style =
  1. | LetStyle
  2. | IfStyle
  3. | LetPatternStyle
  4. | MatchStyle
  5. | RegularStyle
type !'a cast_type =
  1. | CastConv of 'a
  2. | CastVM of 'a
  3. | CastCoerce
  4. | CastNative of 'a
type quantified_hypothesis =
  1. | AnonHyp of int
  2. | NamedHyp of Names.Id.t
type !'a explicit_bindings = (quantified_hypothesis * 'a) Loc.located 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 or_var =
  1. | ArgArg of 'a
  2. | ArgVar of Names.Id.t Loc.located
type !'a and_short_name = 'a * Names.Id.t Loc.located option
type !'a or_by_notation =
  1. | AN of 'a
  2. | ByNotation of (string * string option) Loc.located
type module_kind =
  1. | Module
  2. | ModType
  3. | ModAny
type direction_flag = bool
type evars_flag = bool
type rec_flag = bool
type advanced_flag = bool
type letin_flag = bool
type clear_flag = bool option
type multi =
  1. | Precisely of int
  2. | UpTo of int
  3. | RepeatStar
  4. | RepeatPlus
type !'a core_destruction_arg =
  1. | ElimOnConstr of 'a
  2. | ElimOnIdent of Names.Id.t Loc.located
  3. | ElimOnAnonHyp of int
type !'a destruction_arg = clear_flag * 'a core_destruction_arg
type inversion_kind =
  1. | SimpleInversion
  2. | FullInversion
  3. | FullInversionClear
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