]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/CoRN-Decl/algebra/Cauchy_COF.ma
- transcript: patched to generate aliases instead of inlined variables
[helm.git] / helm / software / matita / contribs / CoRN-Decl / algebra / Cauchy_COF.ma
index 46cfc76471e8b0a26114e1fbac536587458c92f9..bbf6cda597e8b51909b0ef8b3ba82052b137e77f 100644 (file)
@@ -38,7 +38,7 @@ field [F], we can define a new ordered field of Cauchy sequences over [F].
 Section Structure
 *)
 
-inline "cic:/CoRN/algebra/Cauchy_COF/Structure/F.var" "Structure__".
+alias id "F" = "cic:/CoRN/algebra/Cauchy_COF/Structure/F.var".
 
 (*#*
 ** Setoid Structure