freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / CoRN-Decl / metrics / Prod_Sub.ma

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 f30b3c65d7f6038f88d9f7f03650e50430cab8aa..46746e6f4cdff8f26c97f0b8fb7ceae83e6c1a58 100644 (file)
--- 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
 *)