X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fmetrics%2FCPseudoMSpaces.ma;h=7b64208ff81a7f98bd2af521695bb4d1d63b11b3;hb=16d0ba4a14fd6bede3e8b3520af7deaefb4f8068;hp=93a5a663f1814ab8f363c8c51754a1b910680d50;hpb=5e01cba364607e7937aec2e359c34f049bb0f108;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN-Decl/metrics/CPseudoMSpaces.ma b/helm/software/matita/contribs/CoRN-Decl/metrics/CPseudoMSpaces.ma
index 93a5a663f..7b64208ff 100644
--- a/helm/software/matita/contribs/CoRN-Decl/metrics/CPseudoMSpaces.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/metrics/CPseudoMSpaces.ma
@@ -35,9 +35,9 @@ Let [A : CSetoid], [d : (CSetoid_bin_fun A A IR)].
 %\end{convention}%
 *)
 
-inline "cic:/CoRN/metrics/CPseudoMSpaces/Relations/A.var" "Relations__".
+alias id "A" = "cic:/CoRN/metrics/CPseudoMSpaces/Relations/A.var".
 
-inline "cic:/CoRN/metrics/CPseudoMSpaces/Relations/d.var" "Relations__".
+alias id "d" = "cic:/CoRN/metrics/CPseudoMSpaces/Relations/d.var".
 
 (* UNEXPORTED
 Set Implicit Arguments.
@@ -111,7 +111,7 @@ Let [A] be a pseudo metric space.
 %\end{convention}%
 *)
 
-inline "cic:/CoRN/metrics/CPseudoMSpaces/PsMS_axioms/A.var" "PsMS_axioms__".
+alias id "A" = "cic:/CoRN/metrics/CPseudoMSpaces/PsMS_axioms/A.var".
 
 inline "cic:/CoRN/metrics/CPseudoMSpaces/CPsMetricSpace_is_CPsMetricSpace.con".
 
@@ -137,7 +137,7 @@ Let [Y] be a pseudo metric space.
 %\end{convention}%
 *)
 
-inline "cic:/CoRN/metrics/CPseudoMSpaces/PsMS_basics/Y.var" "PsMS_basics__".
+alias id "Y" = "cic:/CoRN/metrics/CPseudoMSpaces/PsMS_basics/Y.var".
 
 inline "cic:/CoRN/metrics/CPseudoMSpaces/rev_tri_ineq.con".