X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Findexing.ml;h=925aab6e05d3663ba3d01eabca3cf11e43b16ac8;hb=e8f64678cc425f19336ff4f905f9b2f00acd6627;hp=e72ed64dad3c37c9620a97ec7576784bf3cb80ae;hpb=08a92d276c5477968b02f31097b6ed03185f34eb;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index e72ed64da..925aab6e0 100644
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -728,6 +728,7 @@ let rec betaexpand_term
   let res, lifted_term = 
     match term with
     | C.Meta (i, l) ->
+        let l = [] in
         let l', lifted_l =
           List.fold_right
             (fun arg (res, lifted_tl) ->
@@ -1057,11 +1058,23 @@ let superposition_left (metasenv, context, ugraph) table goal =
     Utils.compare_weights ~normalize:true
       (Utils.weight_of_term l) (Utils.weight_of_term r)
   in
-  let big,small,possmall = 
-    match c with Utils.Gt -> l,r,Utils.Right | _ -> r,l,Utils.Left
-  in
-  let expansions, _ = betaexpand_term menv context ugraph table 0 big in
-  List.map (build_newgoal context goal possmall Equality.SuperpositionLeft) expansions
+  
+  if c = Utils.Incomparable then
+    let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
+    let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
+    prerr_endline "ZZZ";
+    prerr_endline (string_of_int (List.length expansionsl));
+    prerr_endline (string_of_int (List.length expansionsr));
+    List.map (build_newgoal context goal Utils.Right Equality.SuperpositionLeft) expansionsl
+    @
+    List.map (build_newgoal context goal Utils.Left Equality.SuperpositionLeft) expansionsr
+
+  else
+    let big,small,possmall = 
+      match c with Utils.Gt -> l,r,Utils.Right | _ -> r,l,Utils.Left
+    in
+    let expansions, _ = betaexpand_term menv context ugraph table 0 big in
+    List.map (build_newgoal context goal possmall Equality.SuperpositionLeft) expansions
 ;;
 
 (** demodulation, when the target is a goal *)