fixed uris

diff --git a/helm/software/matita/dama_didactic/Makefile b/helm/software/matita/dama_didactic/Makefile
new file mode 100644 (file)
index 0000000..cce033f
--- /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 bed8ec6b1a0b1f21d3e790cf3281d4212f20a090..161063b426341ca18c2c8d6b6723287f35749d1f 100644 (file)
--- 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 (file)
index 0000000..f96fe39
--- /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 9619b94ba2b83d46b93cf122254d8e01e1ca42a2..5c2e734c0697037a686f42c3257b25f377a23635 100644 (file)
--- 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 b451a0acce5dbf0eb92008cb2f4687cc20fad5d1..6ce9b9f31d35ceb9c578fb7c0fdfded4029d24b9 100644 (file)
--- 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 61952d1b096636c51d30ea702971f06d2220a36e..fcefda2448b1537a81b0c86e9a90f82127f364ef 100644 (file)
--- 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 (file)
index ce86d13..0000000
--- 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 966747c766fe81cc1f1baf76295d008bdb56fd55..7d8a068c8e4c48a3d09a7a38286802e789a73cf2 100644 (file)
--- 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 (file)
index 0000000..2d3086b
--- /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 66b64e5bca76741c20871eba3dd1db137b0c6dc9..7e558030caee8edfa366577fcb70ec577fdaac1d 100644 (file)
--- 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".