X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Fmetrics%2FCPseudoMSpaces.ma;h=7b64208ff81a7f98bd2af521695bb4d1d63b11b3;hb=810db29f760117d933ee1f74328043b8fce43847;hp=93a5a663f1814ab8f363c8c51754a1b910680d50;hpb=62596f4e0a109e43c9df5da20571827c8b905ce4;p=helm.git

diff --git a/matita/contribs/CoRN-Decl/metrics/CPseudoMSpaces.ma b/matita/contribs/CoRN-Decl/metrics/CPseudoMSpaces.ma
index 93a5a663f..7b64208ff 100644
--- a/matita/contribs/CoRN-Decl/metrics/CPseudoMSpaces.ma
+++ b/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".