- transcript: patched to generate aliases instead of inlined variables

[helm.git] / helm / software / matita / contribs / CoRN-Decl / metrics / CPseudoMSpaces.ma

diff --git a/helm/software/matita/contribs/CoRN-Decl/metrics/CPseudoMSpaces.ma b/helm/software/matita/contribs/CoRN-Decl/metrics/CPseudoMSpaces.ma
index 93a5a663f1814ab8f363c8c51754a1b910680d50..7b64208ff81a7f98bd2af521695bb4d1d63b11b3 100644 (file)
--- 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".