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]