let check_close
  (_config: config)
  (_subst: subst)
  (context_unifier_space: context_unifier_space)
  (context_partners: context_partners)
  : raw_context_unifier option =

  (* precheck in context_unifier_check assures that
     check_close is only called with an empty remainder *)
  if true (*(Config.is_horn config) || not (Context_unifier.is_remainder' subst)*) then begin
    let closing_context_unifier =
      Context_unifier.create_context_unifier
        context_unifier_space
        (Array.copy context_partners)
        false
    in
      Some closing_context_unifier
  end

  else
    None