aboutsummaryrefslogtreecommitdiff
path: root/contrib/xml/doubleTypeInference.mli
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