Module Declare.Recthm
type t
=
{
name : Names.Id.t;
Name of theorem
typ : Constr.t;
Type of theorem
args : Names.Name.t list;
Names to pre-introduce
impargs : Impargs.manual_implicits;
Explicitily declared implicit arguments
}
Declare.Recthm
type t
=
{
name : Names.Id.t; | Name of theorem |
typ : Constr.t; | Type of theorem |
args : Names.Name.t list; | Names to pre-introduce |
impargs : Impargs.manual_implicits; | Explicitily declared implicit arguments |
}