coq 8.7.1 · OCaml Package

coq

type notation = string

type explicitation =

| ExplByPos of int * Names.Id.t option
| ExplByName of Names.Id.t

type binder_kind =

| Default of Decl_kinds.binding_kind
| Generalized of Decl_kinds.binding_kind * Decl_kinds.binding_kind * bool

type abstraction_kind =

| AbsLambda
| AbsPi

type proj_flag = int option

type sign = bool

type raw_natural_number = string

type prim_token =

| Numeral of raw_natural_number * sign
| String of string

type instance_expr = Misctypes.glob_level list

type cases_pattern_expr_r =

| CPatAlias of cases_pattern_expr * Names.Id.t
| CPatCstr of Libnames.reference * cases_pattern_expr list option * cases_pattern_expr list
| CPatAtom of Libnames.reference option
| CPatOr of cases_pattern_expr list
| CPatNotation of notation * cases_pattern_notation_substitution * cases_pattern_expr list
| CPatPrim of prim_token
| CPatRecord of (Libnames.reference * cases_pattern_expr) list
| CPatDelimiters of string * cases_pattern_expr
| CPatCast of cases_pattern_expr * constr_expr

and cases_pattern_expr = cases_pattern_expr_r CAst.t

and cases_pattern_notation_substitution =
  cases_pattern_expr list * cases_pattern_expr list list

and constr_expr_r =

| CRef of Libnames.reference * instance_expr option
| CFix of Names.Id.t Loc.located * fix_expr list
| CCoFix of Names.Id.t Loc.located * cofix_expr list
| CProdN of binder_expr list * constr_expr
| CLambdaN of binder_expr list * constr_expr
| CLetIn of Names.Name.t Loc.located * constr_expr * constr_expr option * constr_expr
| CAppExpl of proj_flag * Libnames.reference * instance_expr option * constr_expr list
| CApp of proj_flag * constr_expr * (constr_expr * explicitation Loc.located option) list
| CRecord of (Libnames.reference * constr_expr) list
| CCases of Misctypes.case_style * constr_expr option * case_expr list * branch_expr list
| CLetTuple of Names.Name.t Loc.located list * Names.Name.t Loc.located option * constr_expr option * constr_expr * constr_expr
| CIf of constr_expr * Names.Name.t Loc.located option * constr_expr option * constr_expr * constr_expr
| CHole of Evar_kinds.t option * Misctypes.intro_pattern_naming_expr * Genarg.raw_generic_argument option
| CPatVar of Misctypes.patvar
| CEvar of Glob_term.existential_name * (Names.Id.t * constr_expr) list
| CSort of Misctypes.glob_sort
| CCast of constr_expr * constr_expr Misctypes.cast_type
| CNotation of notation * constr_notation_substitution
| CGeneralization of Decl_kinds.binding_kind * abstraction_kind option * constr_expr
| CPrim of prim_token
| CDelimiters of string * constr_expr

and constr_expr = constr_expr_r CAst.t

and case_expr =
  constr_expr * Names.Name.t Loc.located option * cases_pattern_expr option

and branch_expr =
  (cases_pattern_expr list Loc.located list * constr_expr) Loc.located

and binder_expr = Names.Name.t Loc.located list * binder_kind * constr_expr

and fix_expr =
  Names.Id.t Loc.located
  * (Names.Id.t Loc.located option * recursion_order_expr)
  * local_binder_expr list
  * constr_expr
  * constr_expr

and cofix_expr =
  Names.Id.t Loc.located * local_binder_expr list * constr_expr * constr_expr

and recursion_order_expr =

| CStructRec
| CWfRec of constr_expr
| CMeasureRec of constr_expr * constr_expr option

and local_binder_expr =

| CLocalAssum of Names.Name.t Loc.located list * binder_kind * constr_expr
| CLocalDef of Names.Name.t Loc.located * constr_expr * constr_expr option
| CLocalPattern of (cases_pattern_expr * constr_expr option) Loc.located

and constr_notation_substitution =
  constr_expr list * constr_expr list list * local_binder_expr list list

type typeclass_constraint =
  (Names.Name.t Loc.located * Names.Id.t Loc.located list option)
  * Decl_kinds.binding_kind
  * constr_expr

and typeclass_context = typeclass_constraint list

type constr_pattern_expr = constr_expr

type with_declaration_ast =

| CWith_Module of Names.Id.t list Loc.located * Libnames.qualid Loc.located
| CWith_Definition of Names.Id.t list Loc.located * constr_expr

type module_ast_r =

| CMident of Libnames.qualid
| CMapply of module_ast * module_ast
| CMwith of module_ast * with_declaration_ast

and module_ast = module_ast_r CAst.t

package coq