X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=b3a53d92953f61e2f86dad7baf146deab69dec79;hb=f5943d511ac074948a317bb35b35faa6ad508c4e;hp=02b080147aa2c0ccbafaf1529137840c700c566c;hpb=32d6065811881d4ceac52448330ae793840e14e8;p=helm.git

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index 02b080147..b3a53d929 100644
--- 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