]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/paramodulation/Makefile
fixed LApply pretty printing
[helm.git] / helm / ocaml / paramodulation / Makefile
index be59fc135aad2d9fe0f972c677b2d90f79afd6b2..9d30e7020d39fb9f1da56ec8dfbf1e6f6110b3d6 100644 (file)
@@ -27,22 +27,28 @@ opt: saturation.opt
 
 INTERFACE_FILES = \
        utils.mli \
-       inference.mli
+       inference.mli 
 
 DEPOBJS = \
        $(INTERFACE_FILES) $(INTERFACE_FILES:%.mli=%.ml) \
+       trie.ml \
        path_indexing.ml \
+       discrimination_tree.ml \
+       test_indexing.ml \
        indexing.ml \
-       saturation.ml \
-       test_path_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 \
-       test_path_indexing.cmo
+       discrimination_tree.cmo \
+       test_indexing.cmo
 # REGTESTOBJS = $(TESTOBJS) regtest.cmo
 # TESTLIBOBJS = $(TESTOBJS) testlibrary.cmo
 
@@ -57,7 +63,7 @@ saturation: $(TOPLEVELOBJS) $(LIBRARIES)
 saturation.opt: $(TOPLEVELOBJS:.cmo=.cmx) $(LIBRARIES_OPT)
        $(OCAMLOPT) -thread -linkpkg -o $@ $(TOPLEVELOBJS:.cmo=.cmx)
 
-test_path_indexing: $(TESTOBJS) $(TEST_LIBRARIES)
+test_indexing: $(TESTOBJS) $(TEST_LIBRARIES)
        $(OCAMLC) -linkpkg -o $@ $(TESTOBJS)
 
 .SUFFIXES: .ml .mli .cmo .cmi .cmx