X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_paramodulation%2Findex.ml;h=49af5e08946b5e72066e1d35428e079a084885ee;hb=446bec03de2d1e48ee612cd8020777aeeb7fbf06;hp=36c9dd75e693ec51cf5e168995563113c2b92f66;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/components/ng_paramodulation/index.ml b/matita/components/ng_paramodulation/index.ml
index 36c9dd75e..49af5e089 100644
--- a/matita/components/ng_paramodulation/index.ml
+++ b/matita/components/ng_paramodulation/index.ml
@@ -49,7 +49,8 @@ module Index(B : Orderings.Blob) = struct
           | Terms.Node (Terms.Var _::_) ->
 	      assert false *)
           | Terms.Node ([] | [ _ ] ) -> assert false
-          | Terms.Node (Terms.Node _::_) -> assert false	      
+          (* FIXME : if we can have a variable we can also have a term 
+            | Terms.Node (Terms.Node _::_) as t -> assert false	 *)      
           | Terms.Node (hd::tl) ->
               aux (List.length tl) hd @ List.flatten (List.map (aux 0) tl) 
         in