fixed proof generation again

[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 da76559e843f6f16ec80be9c78cb671b085aa647..e4dec639749adff715b48e7ce993d7d4ca45296c 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -399,7 +399,7 @@ let subsumption_aux use_unification env table target =
           in
           (match Subst.merge_subst_if_possible subst subst' with
           | None -> ok what leftorright tl
-          | Some s -> Some (s, equation, leftorright))
+          | Some s -> Some (s, equation, leftorright <> pos ))
         with 
         | Inference.MatchingFailure 
         | CicUnification.UnificationFailure _ -> ok what leftorright tl