From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 1 Dec 2006 18:25:40 +0000 (+0000)
Subject: some uris fixed
X-Git-Tag: make_still_working~6612
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0fadcf36d82e4ed816a50db09dfd1559a8507e6c;p=helm.git

some uris fixed
---

diff --git a/helm/software/matita/library/Fsub/defn.ma b/helm/software/matita/library/Fsub/defn.ma
index ef94097fb..7f2154893 100644
--- a/helm/software/matita/library/Fsub/defn.ma
+++ b/helm/software/matita/library/Fsub/defn.ma
@@ -94,15 +94,15 @@ notation "hvbox(s break \mapsto t)"
   right associative with precedence 55
   for @{ 'arrow $s $t }.
 
-interpretation "universal type" 'forall S T = (cic:/matita/test/Typ.ind#xpointer(1/1/5) S T).
+interpretation "universal type" 'forall S T = (cic:/matita/Fsub/defn/Typ.ind#xpointer(1/1/5) S T).
 
-interpretation "bound var" 'var x = (cic:/matita/test/Typ.ind#xpointer(1/1/1) x).
+interpretation "bound var" 'var x = (cic:/matita/Fsub/defn/Typ.ind#xpointer(1/1/1) x).
 
-interpretation "bound tvar" 'tvar x = (cic:/matita/test/Typ.ind#xpointer(1/1/3) x).
+interpretation "bound tvar" 'tvar x = (cic:/matita/Fsub/defn/Typ.ind#xpointer(1/1/3) x).
 
-interpretation "bound tname" 'tname x = (cic:/matita/test/Typ.ind#xpointer(1/1/2) x).
+interpretation "bound tname" 'tname x = (cic:/matita/Fsub/defn/Typ.ind#xpointer(1/1/2) x).
 
-interpretation "arrow type" 'arrow S T = (cic:/matita/test/Typ.ind#xpointer(1/1/4) S T). 
+interpretation "arrow type" 'arrow S T = (cic:/matita/Fsub/defn/Typ.ind#xpointer(1/1/4) S T). 
 
 (*** Various kinds of substitution, not all will be used probably ***)
 
@@ -1323,4 +1323,4 @@ lapply (decidable_eq_nat X X1);elim Hletin
             rewrite < Hletin2 in H12;rewrite < H14 in H12;lapply (H5 H12);
             elim Hletin3]
         |rewrite > subst_O_nat;apply in_FV_subst;assumption]]]
-qed.
\ No newline at end of file
+qed.
diff --git a/helm/software/matita/library/Fsub/part1a.ma b/helm/software/matita/library/Fsub/part1a.ma
index 622b8f702..21fa35aa0 100644
--- a/helm/software/matita/library/Fsub/part1a.ma
+++ b/helm/software/matita/library/Fsub/part1a.ma
@@ -13,10 +13,10 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/Fsub/part1a/".
-include "library/logic/equality.ma".
-include "library/nat/nat.ma".
-include "library/datatypes/bool.ma".
-include "library/nat/compare.ma".
+include "logic/equality.ma".
+include "nat/nat.ma".
+include "datatypes/bool.ma".
+include "nat/compare.ma".
 include "Fsub/defn.ma".
 
 theorem JS_Refl : \forall T,G.(WFType G T) \to (WFEnv G) \to (JSubtype G T T).
@@ -377,4 +377,4 @@ theorem JS_narrow : \forall G1,G2,X,P,Q,T,U.
                        (JSubtype (G2 @ (mk_bound true X P :: G1)) T U).
 intros;elim (JS_trans_narrow (t_len Q));apply (H3 ? ? ? ? ? ? ? ? H H1);
 constructor 1;
-qed.
\ No newline at end of file
+qed.
diff --git a/helm/software/matita/library/logic/equality.ma b/helm/software/matita/library/logic/equality.ma
index 2dc6cb435..12c797631 100644
--- a/helm/software/matita/library/logic/equality.ma
+++ b/helm/software/matita/library/logic/equality.ma
@@ -1,5 +1,5 @@
 (**************************************************************************)
-(*       ___	                                                            *)
+(*       ___	                                                          *)
 (*      ||M||                                                             *)
 (*      ||A||       A project by Andrea Asperti                           *)
 (*      ||T||                                                             *)
diff --git a/helm/software/matita/tests/apply2.ma b/helm/software/matita/tests/apply2.ma
index 220eddb4b..db87636d7 100644
--- a/helm/software/matita/tests/apply2.ma
+++ b/helm/software/matita/tests/apply2.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/test/apply2".
+set "baseuri" "cic:/matita/tests/apply2".
 
 include "nat/nat.ma".
 
diff --git a/helm/software/matita/tests/applys.ma b/helm/software/matita/tests/applys.ma
index 1115eaf92..a26594613 100644
--- a/helm/software/matita/tests/applys.ma
+++ b/helm/software/matita/tests/applys.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/test/applys".
+set "baseuri" "cic:/matita/tests/applys".
 
 include "nat/div_and_mod.ma".
 include "nat/factorial.ma".
diff --git a/helm/software/matita/tests/continuationals.ma b/helm/software/matita/tests/continuationals.ma
index f45061bad..bb531961a 100644
--- a/helm/software/matita/tests/continuationals.ma
+++ b/helm/software/matita/tests/continuationals.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/test/continuationals/".
+set "baseuri" "cic:/matita/tests/continuationals".
 include "legacy/coq.ma".
 
 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
diff --git a/helm/software/matita/tests/decl.ma b/helm/software/matita/tests/decl.ma
index a9d083b64..4b67f551a 100644
--- a/helm/software/matita/tests/decl.ma
+++ b/helm/software/matita/tests/decl.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/test/decl".
+set "baseuri" "cic:/matita/tests/decl".
 
 include "nat/times.ma".
 include "nat/orders.ma".
@@ -203,4 +203,4 @@ theorem easy6: ∀t. O ≮ O → O < size t → t ≠ Empty.
      destruct absurd.
      by final
    done.
-qed.
\ No newline at end of file
+qed.
diff --git a/helm/software/matita/tests/dependent_injection.ma b/helm/software/matita/tests/dependent_injection.ma
index ebadd3c2e..28991acf4 100644
--- a/helm/software/matita/tests/dependent_injection.ma
+++ b/helm/software/matita/tests/dependent_injection.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/test/dependent_injection/".
+set "baseuri" "cic:/matita/tests/dependent_injection".
 
 include "legacy/coq.ma".
 
diff --git a/helm/software/matita/tests/injection.ma b/helm/software/matita/tests/injection.ma
index b8ddeaa17..69edcf620 100644
--- a/helm/software/matita/tests/injection.ma
+++ b/helm/software/matita/tests/injection.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/test/injection/".
+set "baseuri" "cic:/matita/tests/injection".
 
 include "legacy/coq.ma".
 
diff --git a/helm/software/matita/tests/naiveparamod.ma b/helm/software/matita/tests/naiveparamod.ma
index 7a3e3914e..3f0c21030 100644
--- a/helm/software/matita/tests/naiveparamod.ma
+++ b/helm/software/matita/tests/naiveparamod.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/test/".
+set "baseuri" "cic:/matita/tests/naiveparamod".
 
 include "logic/equality.ma".
 
diff --git a/helm/software/matita/tests/paramodulation/group.ma b/helm/software/matita/tests/paramodulation/group.ma
index cd49860fc..97e2afe17 100644
--- a/helm/software/matita/tests/paramodulation/group.ma
+++ b/helm/software/matita/tests/paramodulation/group.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/test/paramodulation/group".
+set "baseuri" "cic:/matita/tests/paramodulation/group".
 
 include "legacy/coq.ma".
 
diff --git a/helm/software/matita/tests/pullback.ma b/helm/software/matita/tests/pullback.ma
index 228d27d47..935a90dcf 100644
--- a/helm/software/matita/tests/pullback.ma
+++ b/helm/software/matita/tests/pullback.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/test/".
+set "baseuri" "cic:/matita/tests/pullback".
 
 inductive T : Type \def t : T.
 inductive L : Type \def l : L.
@@ -31,12 +31,12 @@ definition P2_to_L : P2 \to L \def \lambda x.l.
 definition P2_to_R : P2 \to R \def \lambda x.r.
 definition P1_to_P1 : P1 \to P1 \def \lambda x.p1.
 
-coercion cic:/matita/test/L_to_T.con.
-coercion cic:/matita/test/R_to_T.con.
-coercion cic:/matita/test/P1_to_L.con.
-coercion cic:/matita/test/P1_to_R1.con.
-coercion cic:/matita/test/R1_to_R.con.
-coercion cic:/matita/test/R1_to_P2.con.
-coercion cic:/matita/test/P2_to_L.con.
-coercion cic:/matita/test/P2_to_R.con.
-coercion cic:/matita/test/P1_to_P1.con.
+coercion cic:/matita/tests/pullback/L_to_T.con.
+coercion cic:/matita/tests/pullback/R_to_T.con.
+coercion cic:/matita/tests/pullback/P1_to_L.con.
+coercion cic:/matita/tests/pullback/P1_to_R1.con.
+coercion cic:/matita/tests/pullback/R1_to_R.con.
+coercion cic:/matita/tests/pullback/R1_to_P2.con.
+coercion cic:/matita/tests/pullback/P2_to_L.con.
+coercion cic:/matita/tests/pullback/P2_to_R.con.
+coercion cic:/matita/tests/pullback/P1_to_P1.con.
diff --git a/helm/software/matita/tests/tinycals.ma b/helm/software/matita/tests/tinycals.ma
index 960051672..465d7c06e 100644
--- a/helm/software/matita/tests/tinycals.ma
+++ b/helm/software/matita/tests/tinycals.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/test/tinycals".
+set "baseuri" "cic:/matita/tests/tinycals".
 
 theorem prova: 
   \forall A,B,C:Prop.