X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fmetrics%2FCMetricSpaces.ma;h=45f6ff0c6e98416aba0c5c1878da32aad358db4d;hb=3cf6181bded05eb63140d1b2ba4f2f5791a73b48;hp=3b0591a8028ea9601b1bee1af4305aefd7d99916;hpb=80110e17ef1d38d71473e9471ce15beddde663bb;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN-Decl/metrics/CMetricSpaces.ma b/helm/software/matita/contribs/CoRN-Decl/metrics/CMetricSpaces.ma
index 3b0591a80..45f6ff0c6 100644
--- a/helm/software/matita/contribs/CoRN-Decl/metrics/CMetricSpaces.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/metrics/CMetricSpaces.ma
@@ -25,7 +25,7 @@ include "metrics/Prod_Sub.ma".
 include "metrics/Equiv.ma".
 
 (* UNEXPORTED
-Section Definition_MS.
+Section Definition_MS
 *)
 
 (*#* **Definition of Metric Space
@@ -33,14 +33,14 @@ Section Definition_MS.
 
 inline "cic:/CoRN/metrics/CMetricSpaces/CMetricSpace.ind".
 
-coercion "cic:/matita/CoRN-Decl/metrics/CMetricSpaces/scms_crr.con" 0 (* compounds *).
+coercion cic:/matita/CoRN-Decl/metrics/CMetricSpaces/scms_crr.con 0 (* compounds *).
 
 (* UNEXPORTED
-End Definition_MS.
+End Definition_MS
 *)
 
 (* UNEXPORTED
-Section MS_basics.
+Section MS_basics
 *)
 
 (*#* **Metric Space basics
@@ -53,11 +53,11 @@ inline "cic:/CoRN/metrics/CMetricSpaces/d_zero_imp_eq.con".
 inline "cic:/CoRN/metrics/CMetricSpaces/is_CMetricSpace_diag_zero.con".
 
 (* UNEXPORTED
-End MS_basics.
+End MS_basics
 *)
 
 (* UNEXPORTED
-Section prodandsub.
+Section prodandsub
 *)
 
 (*#* **Product-Metric-Spaces and Sub-Metric-Spaces
@@ -88,11 +88,11 @@ Implicit Arguments SubMetricSpace [X].
 *)
 
 (* UNEXPORTED
-End prodandsub.
+End prodandsub
 *)
 
 (* UNEXPORTED
-Section Zeroff.
+Section Zeroff
 *)
 
 (*#* **Pseudo Metric Spaces vs Metric Spaces
@@ -167,11 +167,11 @@ inline "cic:/CoRN/metrics/CMetricSpaces/Emb.con".
 inline "cic:/CoRN/metrics/CMetricSpaces/Quotient_pres_CMetricSpace.con".
 
 (* UNEXPORTED
-End Zeroff.
+End Zeroff
 *)
 
 (* UNEXPORTED
-Section Limitt.
+Section Limitt
 *)
 
 (*#* **Limit
@@ -200,6 +200,6 @@ inline "cic:/CoRN/metrics/CMetricSpaces/d_wd.con".
 inline "cic:/CoRN/metrics/CMetricSpaces/unique_MSseqLim.con".
 
 (* UNEXPORTED
-End Limitt.
+End Limitt
 *)