X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2FMakefile;h=9d30e7020d39fb9f1da56ec8dfbf1e6f6110b3d6;hb=aa0c24992572f26d8e78ae34b60c7e151167cf49;hp=be59fc135aad2d9fe0f972c677b2d90f79afd6b2;hpb=a89f7271e79dc7dc81dc868a75125669c8decc16;p=helm.git

diff --git a/helm/ocaml/paramodulation/Makefile b/helm/ocaml/paramodulation/Makefile
index be59fc135..9d30e7020 100644
--- a/helm/ocaml/paramodulation/Makefile
+++ b/helm/ocaml/paramodulation/Makefile
@@ -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