package coq

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

type universe_decl_expr =
  (Misctypes.lident list, Misctypes.glob_constraint list)
    Misctypes.gen_universe_decl

type ident_decl = Misctypes.lident * universe_decl_expr option

type name_decl = Misctypes.lname * universe_decl_expr option

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 * Misctypes.lname
| 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 Misctypes.lident * fix_expr list
| CCoFix of Misctypes.lident * cofix_expr list
| CProdN of local_binder_expr list * constr_expr
| CLambdaN of local_binder_expr list * constr_expr
| CLetIn of Misctypes.lname * 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 CAst.t option) list
| CRecord of (Libnames.reference * constr_expr) list
| CCases of Constr.case_style * constr_expr option * case_expr list * branch_expr list
| CLetTuple of Misctypes.lname list * Misctypes.lname option * constr_expr option * constr_expr * constr_expr
| CIf of constr_expr * Misctypes.lname 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 * Misctypes.lname option * cases_pattern_expr option

and branch_expr = (cases_pattern_expr list list * constr_expr) CAst.t

and fix_expr =
  Misctypes.lident
  * (Misctypes.lident option * recursion_order_expr)
  * local_binder_expr list
  * constr_expr
  * constr_expr

and cofix_expr =
  Misctypes.lident * 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 Misctypes.lname list * binder_kind * constr_expr
| CLocalDef of Misctypes.lname * constr_expr * constr_expr option
| CLocalPattern of (cases_pattern_expr * constr_expr option) CAst.t

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

type constr_pattern_expr = constr_expr

type with_declaration_ast =

| CWith_Module of Names.Id.t list CAst.t * Libnames.qualid CAst.t
| CWith_Definition of Names.Id.t list CAst.t * universe_decl_expr option * 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