args removed from equalities.

[helm.git] / components / tactics / paramodulation / inference.mli

diff --git a/components/tactics/paramodulation/inference.mli b/components/tactics/paramodulation/inference.mli
index 5fdf694fc01f4d4777820e979a418891602af593..dd2d4caa17840e1aaf2fbf3b5ac626fcd6897b35 100644 (file)
--- a/components/tactics/paramodulation/inference.mli
+++ b/components/tactics/paramodulation/inference.mli
@@ -32,8 +32,7 @@ type equality =
      Cic.term *          (* left side *)
      Cic.term *          (* right side *)
      Utils.comparison) * (* ordering *)  
-    Cic.metasenv *       (* environment for metas *)
-    Cic.term list        (* arguments *)
+    Cic.metasenv        (* environment for metas *)
 
 and proof =
   | NoProof   (* no proof *)