- proofs by subsumption now add a symmetry step if needed

[helm.git] / helm / software / components / tactics / paramodulation / indexing.ml

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index 524c06eff409542d664256094fc6977bff31d507..da76559e843f6f16ec80be9c78cb671b085aa647 100644 (file)
--- 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 =