BTop is a category.

[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 4e14964ff3dc26016818fecd566e83ced817214c..6942a6884a2dfbecdc71ec18a8e87f37c80786a6 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -587,6 +587,16 @@ exception Foo
 
 (** demodulation, when target is an equality *)
 let rec demodulation_equality bag ?from eq_uri newmeta env table target =
+        (*
+          prerr_endline ("demodulation_eq:\n");
+        Index.iter table (fun l -> 
+          let l = Index.PosEqSet.elements l in
+          let l = 
+            List.map (fun (p,e) -> 
+              Utils.string_of_pos p ^ Equality.string_of_equality e) l in
+          prerr_endline (String.concat "\n" l)
+          );
+          *)
   let module C = Cic in
   let module S = CicSubstitution in
   let module M = CicMetaSubst in