- let l,r,ty =
- match lit with
- | Terms.Equation(l,r,ty,_) -> l,r,ty
- | _ -> assert false
- in
- match deep_eq ~unify:true l r ty [] (fun x -> x) (fun x -> x)
- table (Some(bag,maxvar,clause,Subst.id_subst)) with
- | None -> Some (bag,clause)
- | Some (bag,maxvar,cl,subst) ->
- prerr_endline "Goal subsumed";
- raise (Success (bag,maxvar,cl))
+ if vl = [] then Some (bag,clause)
+ else
+ let l,r,ty =
+ match lit with
+ | Terms.Equation(l,r,ty,_) -> l,r,ty
+ | _ -> assert false
+ in
+ match deep_eq ~unify:true l r ty [] (fun x -> x) (fun x -> x)
+ table (Some(bag,maxvar,clause,Subst.id_subst)) with
+ | None -> Some (bag,clause)
+ | Some (bag,maxvar,cl,subst) ->
+ prerr_endline "Goal subsumed";
+ raise (Success (bag,maxvar,cl))