coq 8.7.1 · OCaml Package

coq

type patvar = Names.Id.t

type !'constr intro_pattern_expr =

| IntroForthcoming of bool
| IntroNaming of intro_pattern_naming_expr
| IntroAction of 'constr intro_pattern_action_expr

and intro_pattern_naming_expr =

| IntroIdentifier of Names.Id.t
| IntroFresh of Names.Id.t
| IntroAnonymous

and !'constr intro_pattern_action_expr =

| IntroWildcard
| IntroOrAndPattern of 'constr or_and_intro_pattern_expr
| IntroInjection of 'constr intro_pattern_expr Loc.located list
| IntroApplyOn of 'constr Loc.located * 'constr intro_pattern_expr Loc.located
| IntroRewrite of bool

and !'constr or_and_intro_pattern_expr =

| IntroOrPattern of 'constr intro_pattern_expr Loc.located list list
| IntroAndPattern of 'constr intro_pattern_expr Loc.located list

type !'id move_location =

| MoveAfter of 'id
| MoveBefore of 'id
| MoveFirst
| MoveLast

type !'a glob_sort_gen =

| GProp
| GSet
| 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 =

| LetStyle
| IfStyle
| LetPatternStyle
| MatchStyle
| RegularStyle

type !'a cast_type =

| CastConv of 'a
| CastVM of 'a
| CastCoerce
| CastNative of 'a

type quantified_hypothesis =

| AnonHyp of int
| NamedHyp of Names.Id.t

type !'a explicit_bindings = (quantified_hypothesis * 'a) Loc.located list

type !'a bindings =

| ImplicitBindings of 'a list
| ExplicitBindings of 'a explicit_bindings
| NoBindings

type !'a with_bindings = 'a * 'a bindings

type !'a or_var =

| ArgArg of 'a
| ArgVar of Names.Id.t Loc.located

type !'a and_short_name = 'a * Names.Id.t Loc.located option

type !'a or_by_notation =

| AN of 'a
| ByNotation of (string * string option) Loc.located

type module_kind =

| Module
| ModType
| 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 =

| Precisely of int
| UpTo of int
| RepeatStar
| RepeatPlus

type !'a core_destruction_arg =

| ElimOnConstr of 'a
| ElimOnIdent of Names.Id.t Loc.located
| ElimOnAnonHyp of int

type !'a destruction_arg = clear_flag * 'a core_destruction_arg

type inversion_kind =

| SimpleInversion
| FullInversion
| FullInversionClear

package coq