some uris fixed

diff --git a/helm/software/matita/library/Fsub/defn.ma b/helm/software/matita/library/Fsub/defn.ma
index ef94097fb18ab94cd3ec4112a22092f3aa9cd779..7f2154893ddde65e5e87dc7ded1f4fe0f110ddb4 100644 (file)
--- 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 622b8f702acf7adfc519663ad710f69fbbba4aaa..21fa35aa0f9e1242c5f4ef406ffa15acf146e14c 100644 (file)
--- 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 2dc6cb435ee610d899c234c5760e3a187b3816cf..12c79763132bd4049492b493cde00e09b106fbbe 100644 (file)
--- 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 220eddb4bc785193c164239f99b19f15e3813e26..db87636d7f89bbcb581e1db99e5365e3b9dbbd3a 100644 (file)
--- 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 1115eaf92110ae94f5bbea0d037ee37d19508191..a265946132ef64cfbbcc5a04c143e3b079105d75 100644 (file)
--- 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 f45061bad76ef276a3e7a8ffbac64f90f1fe0e82..bb531961a3a28c172d7f7275450a0000c60eddc3 100644 (file)
--- 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 a9d083b64cc4eea3198120fbe7a5c7453c1b761f..4b67f551ab6821646c7bda52a445f646504916b4 100644 (file)
--- 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 ebadd3c2ee0223944119f71ef12b83da3dd8d842..28991acf43cfcf55cc07ef6ef3cb5047126d4927 100644 (file)
--- 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 b8ddeaa17f22dd077719e691e760c7fff34931a3..69edcf6205ea8ccaee3fd29d76f05bc7f4b92b06 100644 (file)
--- 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 7a3e3914ed980427f7d58e5c5ba701d631afba11..3f0c21030d182ebbfcdbc3d791aafc290f7833bf 100644 (file)
--- 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 cd49860fc834de136246e4c8490b6f33e640938d..97e2afe179d58ceb9e1d31af594d73bc5dcfd22b 100644 (file)
--- 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 228d27d474df3b617f27405d8d3f6f0d5735743a..935a90dcfda59211665beee8299aef38b743a3ce 100644 (file)
--- 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 9600516722e89ff1648507d0cf0f9bb41fd33dbd..465d7c06e0953702c2b23104c18493e457eae183 100644 (file)
--- 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.