Unify (rocq-runtime.Firstorder_core

module Item : sig ... end

type instance =

| Real of Item.t * int
| Phantom of EConstr.constr

val unif_atoms : 
  check:bool ->
  Formula.Env.t ->
  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