fixed proof generation again

[helm.git] / components / tactics / paramodulation / saturation.ml

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index 02b080147aa2c0ccbafaf1529137840c700c566c..b3a53d92953f61e2f86dad7baf146deab69dec79 100644 (file)
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -896,14 +896,14 @@ let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
       in
 (*      match Indexing.subsumption env table goal_equation with*)
        match Indexing.unification env table goal_equation with 
-        | Some (subst, equality, pos ) ->
+        | Some (subst, equality, swapped ) ->
             prerr_endline 
               ("GOAL SUBSUMED BY: " ^ Equality.string_of_equality equality);
             prerr_endline ("SUBST:" ^ Subst.ppsubst subst);
             let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in
             let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
             let p =
-              if pos = Utils.Left then
+              if swapped then
                 Equality.symmetric eq_ty l id uri m
               else
                 p