package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type lident = Names.lident
  • deprecated use [Names.lident
type lname = Names.lname
  • deprecated use [Names.lname]
type lstring = Names.lstring
  • deprecated use [Names.lstring]
type !'a or_by_notation_r = 'a Constrexpr.or_by_notation_r =
  1. | AN of 'a
    (*
    • deprecated use version in [Constrexpr]
    *)
  2. | ByNotation of string * string option
    (*
    • deprecated use version in [Constrexpr]
    *)
  • deprecated use [Constrexpr.or_by_notation_r]
type !'a or_by_notation = 'a Constrexpr.or_by_notation
  • deprecated use [Constrexpr.or_by_notation]
type intro_pattern_naming_expr = Namegen.intro_pattern_naming_expr =
  1. | IntroIdentifier of Names.Id.t
    (*
    • deprecated Use version in [Namegen]
    *)
  2. | IntroFresh of Names.Id.t
    (*
    • deprecated Use version in [Namegen]
    *)
  3. | IntroAnonymous
    (*
    • deprecated Use version in [Namegen]
    *)
  • deprecated use [Namegen.intro_pattern_naming_expr]
type !'a or_var = 'a Locus.or_var =
  1. | ArgArg of 'a
    (*
    • deprecated Use version in [Locus]
    *)
  2. | ArgVar of Names.lident
    (*
    • deprecated Use version in [Locus]
    *)
  • deprecated use [Locus.or_var]
type quantified_hypothesis = Tactypes.quantified_hypothesis =
  1. | AnonHyp of int
    (*
    • deprecated Use version in [Tactypes]
    *)
  2. | NamedHyp of Names.Id.t
    (*
    • deprecated Use version in [Tactypes]
    *)
  • deprecated use [Tactypes.quantified_hypothesis]
type multi = Equality.multi =
  1. | Precisely of int
    (*
    • deprecated use version in [Equality]
    *)
  2. | UpTo of int
    (*
    • deprecated use version in [Equality]
    *)
  3. | RepeatStar
    (*
    • deprecated use version in [Equality]
    *)
  4. | RepeatPlus
    (*
    • deprecated use version in [Equality]
    *)
  • deprecated use [Equality.multi]
type !'a bindings = 'a Tactypes.bindings =
  1. | ImplicitBindings of 'a list
    (*
    • deprecated use version in [Tactypes]
    *)
  2. | ExplicitBindings of 'a Tactypes.explicit_bindings
    (*
    • deprecated use version in [Tactypes]
    *)
  3. | NoBindings
    (*
    • deprecated use version in [Tactypes]
    *)
  • deprecated use [Tactypes.bindings]
type !'constr intro_pattern_expr = 'constr Tactypes.intro_pattern_expr =
  1. | IntroForthcoming of bool
    (*
    • deprecated use version in [Tactypes]
    *)
  2. | IntroNaming of Namegen.intro_pattern_naming_expr
    (*
    • deprecated use version in [Tactypes]
    *)
  3. | IntroAction of 'constr Tactypes.intro_pattern_action_expr
    (*
    • deprecated use version in [Tactypes]
    *)
and !'constr intro_pattern_action_expr = 'constr Tactypes.intro_pattern_action_expr =
  1. | IntroWildcard
    (*
    • deprecated use [Tactypes]
    *)
  2. | IntroOrAndPattern of 'constr Tactypes.or_and_intro_pattern_expr
    (*
    • deprecated use [Tactypes]
    *)
  3. | IntroInjection of 'constr intro_pattern_expr CAst.t list
    (*
    • deprecated use [Tactypes]
    *)
  4. | IntroApplyOn of 'constr CAst.t * 'constr intro_pattern_expr CAst.t
    (*
    • deprecated use [Tactypes]
    *)
  5. | IntroRewrite of bool
    (*
    • deprecated use [Tactypes]
    *)
and !'constr or_and_intro_pattern_expr = 'constr Tactypes.or_and_intro_pattern_expr =
  1. | IntroOrPattern of 'constr intro_pattern_expr CAst.t list list
    (*
    • deprecated use [Tactypes]
    *)
  2. | IntroAndPattern of 'constr intro_pattern_expr CAst.t list
    (*
    • deprecated use [Tactypes]
    *)
  • deprecated use version in [Tactypes]
type !'id move_location = 'id Logic.move_location =
  1. | MoveAfter of 'id
    (*
    • deprecated use version in [Logic]
    *)
  2. | MoveBefore of 'id
    (*
    • deprecated use version in [Logic]
    *)
  3. | MoveFirst
    (*
    • deprecated use version in [Logic]
    *)
  4. | MoveLast
    (*
    • deprecated use version in [Logic]
    *)
  • deprecated use version in [Logic]
type !'a cast_type = 'a Glob_term.cast_type =
  1. | CastConv of 'a
    (*
    • deprecated use version in [Glob_term]
    *)
  2. | CastVM of 'a
    (*
    • deprecated use version in [Glob_term]
    *)
  3. | CastCoerce
    (*
    • deprecated use version in [Glob_term]
    *)
  4. | CastNative of 'a
    (*
    • deprecated use version in [Glob_term]
    *)
  • deprecated use version in [Glob_term]
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