X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Fequality_indexing.ml;h=4c07731d51f3bb4e46b2c58aa1dce78e181800d4;hb=102b6ad309695168ae95c2d4a9c3daa96599de21;hp=1dffb639947bf7a3eb57af28efd66ef673f03b9d;hpb=bbb2fa6a7f4f329d8ef8dac6ce34bf37dd37c064;p=helm.git

diff --git a/components/tactics/paramodulation/equality_indexing.ml b/components/tactics/paramodulation/equality_indexing.ml
index 1dffb6399..4c07731d5 100644
--- a/components/tactics/paramodulation/equality_indexing.ml
+++ b/components/tactics/paramodulation/equality_indexing.ml
@@ -58,7 +58,7 @@ struct
     ;;
 
     let remove_index tree equality = 
-      let _, _, (_, l, r, ordering), _, _ = equality in
+      let _, _, (_, l, r, ordering), _ = equality in
 	match ordering with
 	  | Utils.Gt -> remove_index tree l (Utils.Left, equality)
 	  | Utils.Lt -> remove_index tree r (Utils.Right, equality)
@@ -67,7 +67,7 @@ struct
 		remove_index tree l (Utils.Left, equality)
 
     let index tree equality = 
-      let _, _, (_, l, r, ordering), _, _ = equality in
+      let _, _, (_, l, r, ordering), _ = equality in
 	match ordering with
 	  | Utils.Gt -> index tree l (Utils.Left, equality)
 	  | Utils.Lt -> index tree r (Utils.Right, equality)
@@ -77,7 +77,7 @@ struct
   
 
     let in_index tree equality = 
-      let _, _, (_, l, r, ordering), _, _ = equality in
+      let _, _, (_, l, r, ordering), _ = equality in
       let meta_convertibility (pos,equality') = 
 	Inference.meta_convertibility_eq equality equality' 
       in
@@ -103,7 +103,7 @@ module PT =
     ;;
 
     let remove_index tree equality = 
-      let _, _, (_, l, r, ordering), _, _ = equality in
+      let _, _, (_, l, r, ordering), _ = equality in
 	  match ordering with
 	  | Utils.Gt -> remove_index tree l (Utils.Left, equality)
 	  | Utils.Lt -> remove_index tree r (Utils.Right, equality)
@@ -112,7 +112,7 @@ module PT =
 		remove_index tree l (Utils.Left, equality)
 
     let index tree equality = 
-      let _, _, (_, l, r, ordering), _, _ = equality in
+      let _, _, (_, l, r, ordering), _ = equality in
 	match ordering with
 	  | Utils.Gt -> index tree l (Utils.Left, equality)
 	  | Utils.Lt -> index tree r (Utils.Right, equality)
@@ -122,7 +122,7 @@ module PT =
   
 
     let in_index tree equality = 
-      let _, _, (_, l, r, ordering), _, _ = equality in
+      let _, _, (_, l, r, ordering), _ = equality in
       let meta_convertibility (pos,equality') = 
 	Inference.meta_convertibility_eq equality equality' 
       in