- transcript: patched to generate aliases instead of inlined variables

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

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 a5ce0fcda94dd651ae36e5452a6a16c2b9ac9bf5..2b12a73bcfc42e6fb3a95b0b9e80d1ce6a21330d 100644 (file)
--- 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".