blob: a934eaa7e7f832532399e4f31cbe5378ec077930 (
plain)
1
2
3
4
5
6
7
8
9
10
|
type types = { synthesized : Term.types; expected : Term.types option; }
val cprop : Names.kernel_name
val whd_betadeltaiotacprop :
Environ.env -> Evd.evar_map -> Term.constr -> Term.constr
val double_type_of :
Environ.env -> Evd.evar_map -> Term.constr -> Term.constr option ->
types Acic.CicHash.t -> unit
|