package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type lident = Names.Id.t CAst.t
type lname = Names.Name.t CAst.t
type lstring = string CAst.t
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 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
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 !'a universe_kind =
  1. | UAnonymous
  2. | UUnknown
  3. | UNamed of 'a
type glob_level = level_info glob_sort_gen
type glob_constraint = glob_level * Univ.constraint_type * glob_level
type sort_info = (Libnames.reference * int) option list
type glob_sort = sort_info glob_sort_gen
type existential_key = Evar.t
type case_style = Constr.case_style =
  1. | LetStyle
  2. | IfStyle
  3. | LetPatternStyle
  4. | MatchStyle
  5. | RegularStyle
  • deprecated Alias for Constr.case_style
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) 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 or_var =
  1. | ArgArg of 'a
  2. | ArgVar of lident
type !'a and_short_name = 'a * lident option
type !'a or_by_notation_r =
  1. | AN of 'a
  2. | ByNotation of string * string option
type !'a or_by_notation = 'a or_by_notation_r CAst.t
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 lident
  3. | ElimOnAnonHyp of int
type !'a destruction_arg = clear_flag * 'a core_destruction_arg
type inversion_kind =
  1. | SimpleInversion
  2. | FullInversion
  3. | FullInversionClear
type (!'a, !'b) gen_universe_decl = {
  1. univdecl_instance : 'a;
  2. univdecl_extensible_instance : bool;
  3. univdecl_constraints : 'b;
  4. univdecl_extensible_constraints : bool;
}
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