X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Ftransc%2FPi.ma;h=af134caa1b743bdc55fda9151e91e143b7e6790f;hb=be527f5bd4acaf530d8843b23e6849fd5211e1fc;hp=3f077c4436569dd336aae4bddb866a491e7e4e08;hpb=80110e17ef1d38d71473e9471ce15beddde663bb;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN-Decl/transc/Pi.ma b/helm/software/matita/contribs/CoRN-Decl/transc/Pi.ma
index 3f077c443..af134caa1 100644
--- a/helm/software/matita/contribs/CoRN-Decl/transc/Pi.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/transc/Pi.ma
@@ -21,7 +21,7 @@ include "CoRN.ma".
 include "transc/SinCos.ma".
 
 (* UNEXPORTED
-Section Properties_of_Pi.
+Section Properties_of_Pi
 *)
 
 (*#* printing Pi %\ensuremath{\pi}% #π# *)
@@ -113,7 +113,7 @@ inline "cic:/CoRN/transc/Pi/HalfPi_gt_pi_seq.con".
 inline "cic:/CoRN/transc/Pi/pos_Pi.con".
 
 (* UNEXPORTED
-End Properties_of_Pi.
+End Properties_of_Pi
 *)
 
 (* UNEXPORTED
@@ -121,7 +121,7 @@ Hint Resolve Cos_HalfPi: algebra.
 *)
 
 (* UNEXPORTED
-Section Pi_and_Order.
+Section Pi_and_Order
 *)
 
 (*#* **Properties of Pi
@@ -180,7 +180,7 @@ inline "cic:/CoRN/transc/Pi/invQuarterPi_less_HalfPi.con".
 inline "cic:/CoRN/transc/Pi/invQuarterPi_less_QuarterPi.con".
 
 (* UNEXPORTED
-End Pi_and_Order.
+End Pi_and_Order
 *)
 
 (* UNEXPORTED
@@ -201,7 +201,7 @@ Ltac PiSolve := try apply less_leEq; auto with piorder.
 (* end hide *)
 
 (* UNEXPORTED
-Section Sin_And_Cos.
+Section Sin_And_Cos
 *)
 
 (*#* **More formulas
@@ -275,7 +275,7 @@ inline "cic:/CoRN/transc/Pi/Cos_periodic.con".
 inline "cic:/CoRN/transc/Pi/Tan_periodic.con".
 
 (* UNEXPORTED
-End Sin_And_Cos.
+End Sin_And_Cos
 *)
 
 (* UNEXPORTED