From ef3e622c49ce8a0478c3ef1326d4f179aff3d1ed Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sun, 23 Mar 2008 18:55:49 +0000
Subject: [PATCH] Fsub moved in contribs

---
 .../{library => contribs/POPLmark}/Fsub/defn.ma  |  0
 .../POPLmark}/Fsub/part1a.ma                     |  0
 .../POPLmark}/Fsub/part1a_inversion.ma           |  0
 .../{library => contribs/POPLmark}/Fsub/util.ma  |  0
 helm/software/matita/contribs/POPLmark/Makefile  | 16 ++++++++++++++++
 helm/software/matita/contribs/POPLmark/depends   |  7 +++++++
 helm/software/matita/contribs/POPLmark/root      |  1 +
 helm/software/matita/library/depends             |  4 ----
 8 files changed, 24 insertions(+), 4 deletions(-)
 rename helm/software/matita/{library => contribs/POPLmark}/Fsub/defn.ma (100%)
 rename helm/software/matita/{library => contribs/POPLmark}/Fsub/part1a.ma (100%)
 rename helm/software/matita/{library => contribs/POPLmark}/Fsub/part1a_inversion.ma (100%)
 rename helm/software/matita/{library => contribs/POPLmark}/Fsub/util.ma (100%)
 create mode 100644 helm/software/matita/contribs/POPLmark/Makefile
 create mode 100644 helm/software/matita/contribs/POPLmark/depends
 create mode 100644 helm/software/matita/contribs/POPLmark/root

diff --git a/helm/software/matita/library/Fsub/defn.ma b/helm/software/matita/contribs/POPLmark/Fsub/defn.ma
similarity index 100%
rename from helm/software/matita/library/Fsub/defn.ma
rename to helm/software/matita/contribs/POPLmark/Fsub/defn.ma
diff --git a/helm/software/matita/library/Fsub/part1a.ma b/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma
similarity index 100%
rename from helm/software/matita/library/Fsub/part1a.ma
rename to helm/software/matita/contribs/POPLmark/Fsub/part1a.ma
diff --git a/helm/software/matita/library/Fsub/part1a_inversion.ma b/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion.ma
similarity index 100%
rename from helm/software/matita/library/Fsub/part1a_inversion.ma
rename to helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion.ma
diff --git a/helm/software/matita/library/Fsub/util.ma b/helm/software/matita/contribs/POPLmark/Fsub/util.ma
similarity index 100%
rename from helm/software/matita/library/Fsub/util.ma
rename to helm/software/matita/contribs/POPLmark/Fsub/util.ma
diff --git a/helm/software/matita/contribs/POPLmark/Makefile b/helm/software/matita/contribs/POPLmark/Makefile
new file mode 100644
index 000000000..a3e891435
--- /dev/null
+++ b/helm/software/matita/contribs/POPLmark/Makefile
@@ -0,0 +1,16 @@
+include ../Makefile.defs
+
+DIR=$(shell basename $$PWD)
+
+$(DIR) all:
+	$(BIN)matitac
+$(DIR).opt opt all.opt:
+	$(BIN)matitac.opt
+clean:
+	$(BIN)matitaclean
+clean.opt:
+	$(BIN)matitaclean.opt
+depend:
+	$(BIN)matitadep
+depend.opt:
+	$(BIN)matitadep.opt
diff --git a/helm/software/matita/contribs/POPLmark/depends b/helm/software/matita/contribs/POPLmark/depends
new file mode 100644
index 000000000..eea5376c2
--- /dev/null
+++ b/helm/software/matita/contribs/POPLmark/depends
@@ -0,0 +1,7 @@
+Fsub/part1a.ma Fsub/defn.ma
+Fsub/util.ma list/list.ma logic/equality.ma nat/compare.ma
+Fsub/defn.ma Fsub/util.ma
+Fsub/part1a_inversion.ma Fsub/defn.ma
+list/list.ma 
+logic/equality.ma 
+nat/compare.ma 
diff --git a/helm/software/matita/contribs/POPLmark/root b/helm/software/matita/contribs/POPLmark/root
new file mode 100644
index 000000000..e6f78ade0
--- /dev/null
+++ b/helm/software/matita/contribs/POPLmark/root
@@ -0,0 +1 @@
+baseuri=cic:/matita
diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends
index a10d64a30..f89dbc335 100644
--- a/helm/software/matita/library/depends
+++ b/helm/software/matita/library/depends
@@ -73,10 +73,6 @@ nat/o.ma nat/binomial.ma nat/sqrt.ma
 Q/Qaxioms.ma Z/compare.ma Z/times.ma nat/iteration2.ma
 Q/q.ma Z/compare.ma Z/plus.ma
 technicalities/setoids.ma datatypes/constructors.ma logic/coimplication.ma logic/connectives2.ma
-Fsub/part1a.ma Fsub/defn.ma
-Fsub/util.ma list/list.ma logic/equality.ma nat/compare.ma
-Fsub/defn.ma Fsub/util.ma
-Fsub/part1a_inversion.ma Fsub/defn.ma
 decidable_kit/streicher.ma logic/connectives.ma logic/equality.ma
 decidable_kit/decidable.ma datatypes/bool.ma decidable_kit/streicher.ma logic/connectives.ma nat/compare.ma
 decidable_kit/fgraph.ma decidable_kit/fintype.ma
-- 
2.39.2