X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Findexing.ml;h=7d981cf316f92611101631e01dceec5e522e7557;hb=d072c3ea699cf33189d18d8431fda9750fc2eb93;hp=7cdbf43d38a2242938c5f83c710f08f3cfe08761;hpb=d990d5c64d0b9c07baef4257e7931321a42ae695;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index 7cdbf43d3..7d981cf31 100644
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -905,6 +905,7 @@ let rec betaexpand_term
          CicTypeChecker.type_of_aux' metasenv context term ugraph 
       in
       let candidates = get_candidates Unification table term in
+      (* List.iter (fun (_,e) -> debug_print (lazy (Equality.string_of_equality e))) candidates; *)
       let r = 
         if subterms_only then 
           [] 
@@ -1176,15 +1177,13 @@ let superposition_left bag (metasenv, context, ugraph) table goal maxmeta =
       prerr_endline (string_of_int (List.length expansionsl));
       prerr_endline (string_of_int (List.length expansionsr));
       *)
-      if expansionsl <> [] then prerr_endline "expansionl";
-      if expansionsr <> [] then prerr_endline "expansionr";
       List.map (build_newgoal bag context goal Utils.Right Equality.SuperpositionLeft) expansionsl
       @
       List.map (build_newgoal bag context goal Utils.Left Equality.SuperpositionLeft) expansionsr
       end
     else
         match c with 
-        | Utils.Gt -> (* prerr_endline "GT"; *) 
+        | Utils.Gt -> 
             let big,small,possmall = l,r,Utils.Right in
             let expansions, _ = betaexpand_term menv context ugraph table 0 big in
             List.map