X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fmetrics%2FProd_Sub.ma;h=46746e6f4cdff8f26c97f0b8fb7ceae83e6c1a58;hb=db235934efa41a0f38e79747f6db4f468367410b;hp=f30b3c65d7f6038f88d9f7f03650e50430cab8aa;hpb=876f16ec4e9080bad4e39bd9c203d6529dcf4f56;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN-Decl/metrics/Prod_Sub.ma b/helm/software/matita/contribs/CoRN-Decl/metrics/Prod_Sub.ma
index f30b3c65d..46746e6f4 100644
--- a/helm/software/matita/contribs/CoRN-Decl/metrics/Prod_Sub.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/metrics/Prod_Sub.ma
@@ -23,7 +23,7 @@ include "CoRN.ma".
 include "metrics/IR_CPMSpace.ma".
 
 (* UNEXPORTED
-Section prodpsmetrics.
+Section prodpsmetrics
 *)
 
 (*#* **Product-Pseudo-Metric-Spaces
@@ -48,11 +48,11 @@ inline "cic:/CoRN/metrics/Prod_Sub/prod0cpsmetricspace_is_CPsMetricSpace.con".
 inline "cic:/CoRN/metrics/Prod_Sub/Prod0CPsMetricSpace.con".
 
 (* UNEXPORTED
-End prodpsmetrics.
+End prodpsmetrics
 *)
 
 (* UNEXPORTED
-Section subpsmetrics.
+Section subpsmetrics
 *)
 
 (*#* **Sub-Pseudo-Metric-Spaces
@@ -126,6 +126,6 @@ Implicit Arguments dsub'_as_cs_fun [X].
 inline "cic:/CoRN/metrics/Prod_Sub/dsub'_uni_continuous''.con".
 
 (* UNEXPORTED
-End subpsmetrics.
+End subpsmetrics
 *)