package coq

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

type obligation_definition_status =

| Define of bool
| Expand

type matching_var_kind =

| FirstOrderPatVar of Misctypes.patvar
| SecondOrderPatVar of Misctypes.patvar

type t =

| ImplicitArg of Globnames.global_reference * int * Names.Id.t option * bool
| BinderType of Names.Name.t
| NamedHole of Names.Id.t
| QuestionMark of obligation_definition_status * Names.Name.t
| CasesType of bool
| InternalHole
| TomatchTypeParameter of Names.inductive * int
| GoalEvar
| ImpossibleCase
| MatchingVar of matching_var_kind
| VarInstance of Names.Id.t
| SubEvar of Constr.existential_key