- transcript: patched to generate aliases instead of inlined variables

[helm.git] / helm / software / matita / contribs / CoRN-Decl / reals / CMetricFields.ma

diff --git a/helm/software/matita/contribs/CoRN-Decl/reals/CMetricFields.ma b/helm/software/matita/contribs/CoRN-Decl/reals/CMetricFields.ma
index 70924e79d46c6bad3f266dcfacd1a7769a3c2686..db445d670b5e9330d610db415a4cf41618629d43 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Decl/reals/CMetricFields.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/reals/CMetricFields.ma
@@ -62,7 +62,7 @@ End basics
 Section CMetric_Field_Cauchy
 *)
 
-inline "cic:/CoRN/reals/CMetricFields/CMetric_Field_Cauchy/F.var" "CMetric_Field_Cauchy__".
+alias id "F" = "cic:/CoRN/reals/CMetricFields/CMetric_Field_Cauchy/F.var".
 
 (*#*
 %\begin{convention}% Let [F:CMetricField].