]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/tactics/paramodulation/indexing.ml
commented some printings
[helm.git] / helm / software / components / tactics / paramodulation / indexing.ml
index 7cdbf43d38a2242938c5f83c710f08f3cfe08761..4745fecc2e5a971bfe53d90510422c4a164d227d 100644 (file)
@@ -1176,8 +1176,10 @@ 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