From a0015ef9513b592bcb709fde08fec85de27de51d Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 14 Jan 2008 09:02:41 +0000
Subject: [PATCH] fixed uris

---
 helm/software/matita/dama_didactic/Makefile   | 14 ++++++++
 helm/software/matita/dama_didactic/bottom.ma  | 18 +++++-----
 helm/software/matita/dama_didactic/depends    | 10 ++++++
 helm/software/matita/dama_didactic/deriv.ma   |  2 +-
 .../software/matita/dama_didactic/ex_deriv.ma |  2 +-
 helm/software/matita/dama_didactic/ex_seq.ma  |  2 +-
 helm/software/matita/dama_didactic/makefile   | 33 -------------------
 helm/software/matita/dama_didactic/reals.ma   |  2 +-
 helm/software/matita/dama_didactic/root       |  2 ++
 .../matita/dama_didactic/sequences.ma         |  2 +-
 10 files changed, 41 insertions(+), 46 deletions(-)
 create mode 100644 helm/software/matita/dama_didactic/Makefile
 create mode 100644 helm/software/matita/dama_didactic/depends
 delete mode 100644 helm/software/matita/dama_didactic/makefile
 create mode 100644 helm/software/matita/dama_didactic/root

diff --git a/helm/software/matita/dama_didactic/Makefile b/helm/software/matita/dama_didactic/Makefile
new file mode 100644
index 000000000..cce033fc0
--- /dev/null
+++ b/helm/software/matita/dama_didactic/Makefile
@@ -0,0 +1,14 @@
+DIR=$(shell basename $$PWD)
+
+$(DIR) all:
+	../matitac
+$(DIR).opt opt all.opt:
+	../matitac.opt
+clean:
+	../matitaclean
+clean.opt:
+	../matitaclean.opt
+depend:
+	../matitadep
+depend.opt:
+	../matitadep.opt
diff --git a/helm/software/matita/dama_didactic/bottom.ma b/helm/software/matita/dama_didactic/bottom.ma
index bed8ec6b1..161063b42 100644
--- a/helm/software/matita/dama_didactic/bottom.ma
+++ b/helm/software/matita/dama_didactic/bottom.ma
@@ -12,11 +12,13 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/test/decl".
+
 
 include "nat/times.ma".
 include "nat/orders.ma".
 
+include "decl.ma".
+
 inductive L (T:Type):Type:=
   bottom: L T
  |j: T → L T.
@@ -29,9 +31,9 @@ notation "hvbox(a break ≡ b)"
 for @{ 'equiv $a $b }.
 
 interpretation "uguaglianza parziale" 'equiv x y =
- (cic:/matita/test/decl/eq.ind#xpointer(1/1) _ x y).
+ (cic:/matita/tests/decl/eq.ind#xpointer(1/1) _ x y).
 
-coercion cic:/matita/test/decl/L.ind#xpointer(1/1/2).
+coercion cic:/matita/tests/decl/L.ind#xpointer(1/1/2).
  
 lemma sim: ∀T:Type. ∀x,y:T. (j ? x) ≡ (j ? y) → (j ? y) ≡ (j ? x).
  intros.
@@ -61,13 +63,13 @@ axiom Rle: L R→L R→Prop.
 axiom Rge: L R→L R→Prop.
 
 interpretation "real plus" 'plus x y =
- (cic:/matita/test/decl/Rplus.con x y).
+ (cic:/matita/tests/decl/Rplus.con x y).
 
 interpretation "real leq" 'leq x y =
- (cic:/matita/test/decl/Rle.con x y).
+ (cic:/matita/tests/decl/Rle.con x y).
 
 interpretation "real geq" 'geq x y =
- (cic:/matita/test/decl/Rge.con x y).
+ (cic:/matita/tests/decl/Rge.con x y).
 
 let rec elev (x:L R) (n:nat) on n: L R ≝
  match n with
@@ -81,7 +83,7 @@ let rec real_of_nat (n:nat) : L R ≝
   | S n ⇒ real_of_nat n + (j ? R1)
   ].
 
-coercion cic:/matita/test/decl/real_of_nat.con.
+coercion cic:/matita/tests/decl/real_of_nat.con.
 
 axiom Rplus_commutative: ∀x,y:R. (j ? x) + (j ? y) ≡ (j ? y) + (j ? x).
 axiom R0_neutral: ∀x:R. (j ? x) + (j ? R0) ≡ (j ? x).
@@ -114,4 +116,4 @@ axiom R2_1: (j ? R1) ≤ S (S O).
 axiom Rdiv_pos: ∀ x,y:R.
  (j ? R0) ≤ (j ? x) → (j ? R1) ≤ (j ? y) → (j ? R0) ≤ Rdiv (j ? x) (j ? y).
 axiom Rle_R0_R1: (j ? R0) ≤ (j ? R1).
-axiom div: ∀x:R. (j ? x) = Rdiv (j ? x) (S (S O)) → (j ? x) = O.
\ No newline at end of file
+axiom div: ∀x:R. (j ? x) = Rdiv (j ? x) (S (S O)) → (j ? x) = O.
diff --git a/helm/software/matita/dama_didactic/depends b/helm/software/matita/dama_didactic/depends
new file mode 100644
index 000000000..f96fe3984
--- /dev/null
+++ b/helm/software/matita/dama_didactic/depends
@@ -0,0 +1,10 @@
+sequences.ma reals.ma
+reals.ma nat/plus.ma
+bottom.ma decl.ma nat/orders.ma nat/times.ma
+deriv.ma reals.ma
+ex_seq.ma sequences.ma
+ex_deriv.ma deriv.ma
+decl.ma 
+nat/orders.ma 
+nat/plus.ma 
+nat/times.ma 
diff --git a/helm/software/matita/dama_didactic/deriv.ma b/helm/software/matita/dama_didactic/deriv.ma
index 9619b94ba..5c2e734c0 100644
--- a/helm/software/matita/dama_didactic/deriv.ma
+++ b/helm/software/matita/dama_didactic/deriv.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/didactic/deriv".
+
 
 include "reals.ma".
 
diff --git a/helm/software/matita/dama_didactic/ex_deriv.ma b/helm/software/matita/dama_didactic/ex_deriv.ma
index b451a0acc..6ce9b9f31 100644
--- a/helm/software/matita/dama_didactic/ex_deriv.ma
+++ b/helm/software/matita/dama_didactic/ex_deriv.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/didactic/ex_deriv".
+
 
 include "deriv.ma".
 
diff --git a/helm/software/matita/dama_didactic/ex_seq.ma b/helm/software/matita/dama_didactic/ex_seq.ma
index 61952d1b0..fcefda244 100644
--- a/helm/software/matita/dama_didactic/ex_seq.ma
+++ b/helm/software/matita/dama_didactic/ex_seq.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/didactic/ex_seq".
+
 
 include "sequences.ma".
 
diff --git a/helm/software/matita/dama_didactic/makefile b/helm/software/matita/dama_didactic/makefile
deleted file mode 100644
index ce86d1360..000000000
--- a/helm/software/matita/dama_didactic/makefile
+++ /dev/null
@@ -1,33 +0,0 @@
-H=@
-
-RT_BASEDIR=../
-OPTIONS=-bench
-MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS)
-CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS) 
-MMAKEO=$(RT_BASEDIR)matitamake.opt $(OPTIONS)
-CLEANO=$(RT_BASEDIR)matitaclean.opt $(OPTIONS) 
-
-devel:=$(shell basename `pwd`)
-
-all: preall
-	$(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel)
-clean: preall
-	$(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel)
-cleanall: preall
-	$(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all
-
-all.opt opt: preall
-	$(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel)
-clean.opt: preall
-	$(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel)
-cleanall.opt: preall
-	$(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEANO) all
-
-%.mo: preall
-	$(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@
-%.mo.opt: preall
-	$(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $(@:.opt=)
-	
-preall:
-	$(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel)
-
diff --git a/helm/software/matita/dama_didactic/reals.ma b/helm/software/matita/dama_didactic/reals.ma
index 966747c76..7d8a068c8 100644
--- a/helm/software/matita/dama_didactic/reals.ma
+++ b/helm/software/matita/dama_didactic/reals.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/didactic/reals".
+
 
 include "nat/plus.ma".
 
diff --git a/helm/software/matita/dama_didactic/root b/helm/software/matita/dama_didactic/root
new file mode 100644
index 000000000..2d3086b02
--- /dev/null
+++ b/helm/software/matita/dama_didactic/root
@@ -0,0 +1,2 @@
+baseuri=cic:/matita/didactic
+include_paths=../tests
diff --git a/helm/software/matita/dama_didactic/sequences.ma b/helm/software/matita/dama_didactic/sequences.ma
index 66b64e5bc..7e558030c 100644
--- a/helm/software/matita/dama_didactic/sequences.ma
+++ b/helm/software/matita/dama_didactic/sequences.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/didactic/sequences".
+
 
 include "reals.ma".
 
-- 
2.39.2