Module Firstorder_plugin.Unify

exception UFAIL of EConstr.constr * EConstr.constr
module Item : sig ... end
type instance =
| Real of Item.t * 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 -> Item.t -> Item.t -> bool