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

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index faae7b15f..b3a53d929 100644
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -882,34 +882,13 @@ let print_goals goals =
            Printf.sprintf "%d: %s" d (String.concat "; " gl')) goals))
 ;;
               
-(* adds a symmetry step *)
-let symmetric pred eq eq_ty l id uri m =
-  let pred = 
-    Cic.Lambda (Cic.Name "Sym",eq_ty,
-     Cic.Appl [CicSubstitution.lift 1 eq ;
-               CicSubstitution.lift 1 eq_ty;
-               Cic.Rel 1;CicSubstitution.lift 1 l]) 
-  in
-  let prefl = 
-    Equality.Exact (Cic.Appl
-      [Cic.MutConstruct(uri,0,1,[]);eq_ty;l]) 
-  in
-  let id1 = 
-    let eq = Equality.mk_equality (0,prefl,(eq_ty,l,l,Eq),m) in
-    let (_,_,_,_,id) = Equality.open_equality eq in
-    id
-  in
-  Equality.Step(Subst.empty_subst,
-    (Equality.Demodulation,id1,(Utils.Left,id),pred))
-;;
-
 let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
 (*
   let names = names_of_context ctx in
   Printf.eprintf "check_goal_subsumed: %s\n" (CicPp.pp ty names);
 *)
   match ty with
-  | Cic.Appl[Cic.MutInd(uri,_,_) as eq;eq_ty;left;right] 
+  | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] 
     when UriManager.eq uri (LibraryObjects.eq_URI ()) ->
       (let goal_equation = 
          Equality.mk_equality
@@ -917,15 +896,15 @@ 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
-                symmetric pred eq eq_ty l id uri m
+              if swapped then
+                Equality.symmetric eq_ty l id uri m
               else
                 p
             in