Module Firstorder_plugin.Unify
exception
UFAIL of EConstr.constr * EConstr.constr
val unif : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> (int * EConstr.constr) list
type instance
=
|
Real of int * EConstr.constr * int
|
Phantom of EConstr.constr
val unif_atoms : Environ.env -> Evd.evar_map -> Constr.metavariable -> EConstr.constr -> EConstr.constr -> EConstr.constr -> instance option
val more_general : Environ.env -> Evd.evar_map -> (int * EConstr.constr) -> (int * EConstr.constr) -> bool