- let is_identity_goal = function
- | _, Terms.Equation (_,_,_,Terms.Eq), _, _ -> Some []
- | _, Terms.Equation (l,r,_,_), vl, proof ->
- (try Some (Unif.unification (* vl *) [] l r)
- with FoUnif.UnificationFailure _ -> None)
- | _, Terms.Predicate _, _, _ -> assert false
- ;;
-
- let build_new_clause_reloc bag maxvar filter rule t subst id id2 pos dir =