some uris fixed

[helm.git] / helm / software / matita / library / Fsub / defn.ma

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.