]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/paramodulation/Makefile
use of discrimination trees instead of path indexes, for a little
[helm.git] / helm / ocaml / paramodulation / Makefile
index f16094a17c7e96af9907c21f146d227b46f40404..9d30e7020d39fb9f1da56ec8dfbf1e6f6110b3d6 100644 (file)
@@ -27,22 +27,25 @@ opt: saturation.opt
 
 INTERFACE_FILES = \
        utils.mli \
-       inference.mli
+       inference.mli 
 
 DEPOBJS = \
        $(INTERFACE_FILES) $(INTERFACE_FILES:%.mli=%.ml) \
+       trie.ml \
        path_indexing.ml \
-       indexing.ml \
-       saturation.ml \
        discrimination_tree.ml \
-       test_indexing.ml
+       test_indexing.ml \
+       indexing.ml \
+       saturation.ml 
 
 TOPLEVELOBJS = $(INTERFACE_FILES:%.mli=%.cmo) \
+       trie.cmo \
        path_indexing.cmo \
        discrimination_tree.cmo \
        indexing.cmo \
        saturation.cmo
 TESTOBJS = $(INTERFACE_FILES:%.mli=%.cmo) \
+       trie.cmo \
        path_indexing.cmo \
        discrimination_tree.cmo \
        test_indexing.cmo