X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FFsub%2Fdefn.ma;h=7f2154893ddde65e5e87dc7ded1f4fe0f110ddb4;hb=0fadcf36d82e4ed816a50db09dfd1559a8507e6c;hp=ef94097fb18ab94cd3ec4112a22092f3aa9cd779;hpb=94b16d13221f5ea3618b453e5f86b787d04d664e;p=helm.git

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.