update in basic_2

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

diff --git a/helm/software/matita/contribs/CoRN-Decl/reals/CauchySeq.ma b/helm/software/matita/contribs/CoRN-Decl/reals/CauchySeq.ma
index 36ca57d6d36c9587183d3a885f741d5c181238bc..4bc6c7aa18e1185dc7bf81a0ffc891253c5e5c09 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Decl/reals/CauchySeq.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/reals/CauchySeq.ma
@@ -43,7 +43,7 @@ Definition IR : CReals := Concrete_R.
 Opaque IR.
 *)
 
-inline "cic:/CoRN/reals/CauchySeq/IR.var".
+alias id "IR" = "cic:/CoRN/reals/CauchySeq/IR.var".
 
 (* NOTATION
 Notation PartIR := (PartFunct IR).