]> matita.cs.unibo.it Git - helm.git/commitdiff
commented some printings
authorEnrico Tassi <enrico.tassi@inria.fr>
Sun, 15 Feb 2009 14:57:16 +0000 (14:57 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Sun, 15 Feb 2009 14:57:16 +0000 (14:57 +0000)
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