X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Findexing.ml;h=da76559e843f6f16ec80be9c78cb671b085aa647;hb=e0c0cfcad2932c0375e5c8379bff43054efe257a;hp=524c06eff409542d664256094fc6977bff31d507;hpb=2aa94b2076ba3772a0ded19110c6f6a4049955a6;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index 524c06eff..da76559e8 100644
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -386,7 +386,7 @@ let subsumption_aux use_unification env table target =
         find_all_matches ~unif_fun
           metasenv context ugraph 0 left ty leftc
   in
-  let rec ok what = function
+  let rec ok what leftorright = function
     | [] -> None
     | (_, subst, menv, ug, ((pos,equation),_))::tl ->
         let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
@@ -398,13 +398,13 @@ let subsumption_aux use_unification env table target =
             unif_fun metasenv m context what' other' ugraph
           in
           (match Subst.merge_subst_if_possible subst subst' with
-          | None -> ok what tl
-          | Some s -> Some (s, equation))
+          | None -> ok what leftorright tl
+          | Some s -> Some (s, equation, leftorright))
         with 
         | Inference.MatchingFailure 
-        | CicUnification.UnificationFailure _ -> ok what tl
+        | CicUnification.UnificationFailure _ -> ok what leftorright tl
   in
-  match ok right leftr with
+  match ok right Utils.Left  leftr with
   | Some _ as res -> res
   | None -> 
       let rightr =
@@ -415,7 +415,7 @@ let subsumption_aux use_unification env table target =
                 find_all_matches ~unif_fun
                   metasenv context ugraph 0 right ty rightc
       in
-        ok left rightr
+        ok left Utils.Right rightr 
 ;;
 
 let subsumption x y z =