X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Freals%2FQ_dense.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Freals%2FQ_dense.ma;h=2b12a73bcfc42e6fb3a95b0b9e80d1ce6a21330d;hb=55444711ececb62f0a93f2a064f64c3b27f744e2;hp=a5ce0fcda94dd651ae36e5452a6a16c2b9ac9bf5;hpb=4609a07e2fe4343d94832fcaf0936223f83ba71c;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN-Decl/reals/Q_dense.ma b/helm/software/matita/contribs/CoRN-Decl/reals/Q_dense.ma
index a5ce0fcda..2b12a73bc 100644
--- a/helm/software/matita/contribs/CoRN-Decl/reals/Q_dense.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/reals/Q_dense.ma
@@ -30,7 +30,7 @@ inline "cic:/CoRN/reals/Q_dense/or_not_and.con".
 Section Interval_definition
 *)
 
-inline "cic:/CoRN/reals/Q_dense/Interval_definition/OF.var" "Interval_definition__".
+alias id "OF" = "cic:/CoRN/reals/Q_dense/Interval_definition/OF.var".
 
 inline "cic:/CoRN/reals/Q_dense/Interval.ind".
 
@@ -63,7 +63,7 @@ Qed.
 Section COrdField_extra
 *)
 
-inline "cic:/CoRN/reals/Q_dense/COrdField_extra/OF.var" "COrdField_extra__".
+alias id "OF" = "cic:/CoRN/reals/Q_dense/COrdField_extra/OF.var".
 
 inline "cic:/CoRN/reals/Q_dense/AbsSmall_pos_reflexive.con".
 
@@ -83,7 +83,7 @@ include "tactics/Opaque_algebra.ma".
 
 (*#*** WARNING: A file is being loaded *****)
 
-inline "cic:/CoRN/reals/Q_dense/Rational_sequence/R1.var" "Rational_sequence__".
+alias id "R1" = "cic:/CoRN/reals/Q_dense/Rational_sequence/R1.var".
 
 inline "cic:/CoRN/reals/Q_dense/start_l.con".