Firstorder_plugin.Unifyexception UFAIL of EConstr.constr * EConstr.constrmodule Item : sig ... endval unif_atoms : Environ.env -> Evd.evar_map -> Constr.metavariable -> EConstr.constr -> Formula.atom -> Formula.atom -> instance optionval more_general : Environ.env -> Evd.evar_map -> Item.t -> Item.t -> bool