X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2FMakefile;h=71abf95d220da622c340d38188eadf646cd8666f;hb=4ea53eb93717cb1bcd6a0ccb7b1a4d711c1c7a9b;hp=38dab9e6b1d929f8d26cb76b11f385e30c2ff0c3;hpb=26d2ecb945a881c61d03f3c259996374209f5d7f;p=helm.git

diff --git a/helm/software/helena/Makefile b/helm/software/helena/Makefile
index 38dab9e6b..71abf95d2 100644
--- a/helm/software/helena/Makefile
+++ b/helm/software/helena/Makefile
@@ -24,7 +24,7 @@ TARGETS = test-si-fast test-si test2-opt test2-byte test3 test6 \
           profile-fast profile profile-coq profile-coq-byte \
           xml-si xml-si-v3 xml xml-v3 \
           export-coq export-matita \
-          export-lp1 export-lp2 export-tj2 export-tj3 export-lyp \
+          export-lp1 export-lp2 export-tj2 export-tj3 export-pts export-lyp \
           matita matitac
 
 include Makefile.common
@@ -49,11 +49,11 @@ OUTPUT = scripts
 
 MA  = grundlagen_2.ma
 V   = grundlagen_2.v
-LP1 = grundlagen_21.elpi
-LP2 = grundlagen_22.elpi
-TJ2 = grundlagen_22.mod
-TJ3 = grundlagen_23.mod
-CC0 = grundlagen_20.elpi
+LP1 = grundlagen_2a_ld3.elpi
+LP2 = grundlagen_2b_ld3.elpi
+TJ2 = grundlagen_2b_ld3.mod
+TJ3 = grundlagen_2c_ld3.mod
+PTS = grundlagen_2b_pts.elpi
 LYP = grundlagen_2b_lyp.elpi
 
 PREAMBLE_MA = ../matita/matita.ma.templ
@@ -146,34 +146,34 @@ xml-v3: $(EXEC).native etc
 
 export-coq $(OUTPUT)/coq/$(V): $(EXEC).native etc
 	@echo "  HELENA -m V8 -q $(INPUT)"
-	$(H)./$(EXEC).native -M $(OUTPUT) -a n -m V8 -p $(PREAMBLE_V) -q $(TEST1) > etc/log.txt
+	$(H)./$(EXEC).native -M $(OUTPUT) -a n -m V8 -p $(PREAMBLE_V) -q $(O) $(TEST1) > etc/log.txt
 
 export-matita $(OUTPUT)/matita/$(MA): $(EXEC).native etc
 	@echo "  HELENA -m MA2 -q $(INPUT)"
-	$(H)./$(EXEC).native -M $(OUTPUT) -a n -m MA2 -p $(PREAMBLE_MA) -q $(TEST1) > etc/log.txt
+	$(H)./$(EXEC).native -M $(OUTPUT) -a n -m MA2 -p $(PREAMBLE_MA) -q $(O) $(TEST1) > etc/log.txt
 
 export-lp1 $(OUTPUT)/lp/$(LP1): $(EXEC).native etc
 	@echo "  HELENA -m LP1 -q $(INPUT)"
-	$(H)./$(EXEC).native -M $(OUTPUT) -a n -m LP1 -p $(PREAMBLE_LP) -q $(TEST1) > etc/log.txt
+	$(H)./$(EXEC).native -M $(OUTPUT) -a n -m LP1 -p $(PREAMBLE_LP) -q $(O) $(TEST1) > etc/log.txt
 
 export-lp2 $(OUTPUT)/lp/$(LP2): $(EXEC).native etc
 	@echo "  HELENA -m LP2 -q $(INPUT)"
-	$(H)./$(EXEC).native -M $(OUTPUT) -a n -m LP2 -p $(PREAMBLE_LP) -q $(TEST1) > etc/log.txt
+	$(H)./$(EXEC).native -M $(OUTPUT) -a n -m LP2 -p $(PREAMBLE_LP) -q $(O) $(TEST1) > etc/log.txt
 
 export-tj2 $(OUTPUT)/lp/$(TJ2): $(EXEC).native etc
 	@echo "  HELENA -m TJ2 -q $(INPUT)"
-	$(H)./$(EXEC).native -M $(OUTPUT) -a n -m TJ2 -p $(PREAMBLE_LP) -q $(TEST1) > etc/log.txt
+	$(H)./$(EXEC).native -M $(OUTPUT) -a n -m TJ2 -p $(PREAMBLE_LP) -q $(O) $(TEST1) > etc/log.txt
 
 export-tj3 $(OUTPUT)/lp/$(TJ3): $(EXEC).native etc
 	@echo "  HELENA -m TJ3 -q $(INPUT)"
-	$(H)./$(EXEC).native -M $(OUTPUT) -a n -m TJ3 -p $(PREAMBLE_LP) -q $(TEST1) > etc/log.txt
+	$(H)./$(EXEC).native -M $(OUTPUT) -a n -m TJ3 -p $(PREAMBLE_LP) -q $(O) $(TEST1) > etc/log.txt
 
-export-cc0 $(OUTPUT)/cc/$(CC0): $(EXEC).native etc
-	@echo "  HELENA -m CC0 -q $(INPUT)"
-	$(H)./$(EXEC).native -M $(OUTPUT) -a n -m CC0 -p $(PREAMBLE_LP) -q $(TEST1) > etc/log.txt
+export-pts $(OUTPUT)/lp/$(PTS): $(EXEC).native etc
+	@echo "  HELENA -m PTS -c -q $(INPUT)"
+	$(H)./$(EXEC).native -M $(OUTPUT) -a n -m PTS -p $(PREAMBLE_LP) -c -q $(O) $(TEST1) > etc/log.txt
 
 export-lyp $(OUTPUT)/lp/$(LYP): $(EXEC).native etc
-	@echo "  HELENA -m lyp -q $(INPUT)"
+	@echo "  HELENA -m lyp -c -q $(INPUT)"
 	$(H)./$(EXEC).native -M $(OUTPUT) -a n -m lyp -p $(PREAMBLE_LP) -c -q $(O) $(TEST1) > etc/log.txt
 
 matita: $(OUTPUT)/matita/$(MA)