Unify (coq-core.Firstorder

exception UFAIL of EConstr.constr * EConstr.constr

type instance =

| Real of int * EConstr.constr * int

| Phantom of EConstr.constr

val unif_atoms : Environ.env -> Evd.evar_map -> Constr.metavariable -> EConstr.constr -> Formula.atom -> Formula.atom -> instance option

val more_general : Environ.env -> Evd.evar_map -> (int * EConstr.constr) -> (int * EConstr.constr) -> bool