X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Freals%2FCauchySeq.ma;h=4bc6c7aa18e1185dc7bf81a0ffc891253c5e5c09;hb=a88be1ca42c0969dbab9a5c76240f5931df876d9;hp=36ca57d6d36c9587183d3a885f741d5c181238bc;hpb=5e01cba364607e7937aec2e359c34f049bb0f108;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN-Decl/reals/CauchySeq.ma b/helm/software/matita/contribs/CoRN-Decl/reals/CauchySeq.ma
index 36ca57d6d..4bc6c7aa1 100644
--- 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).