updated depend files

[helm.git] / matita / components / ng_paramodulation / index.ml

diff --git a/matita/components/ng_paramodulation/index.ml b/matita/components/ng_paramodulation/index.ml
index 36c9dd75e693ec51cf5e168995563113c2b92f66..49af5e08946b5e72066e1d35428e079a084885ee 100644 (file)
--- 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