X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Ftransc%2FPi.ma;h=af134caa1b743bdc55fda9151e91e143b7e6790f;hb=ad45ff0a9bc4ddbfe0691ce1edbfa8784b37aa8e;hp=66c1642002e1e5bec040649b169b4f28ce3f54e1;hpb=94873bb61a663b4fca3dc6d07b7bb9f42122003e;p=helm.git

diff --git a/matita/contribs/CoRN-Decl/transc/Pi.ma b/matita/contribs/CoRN-Decl/transc/Pi.ma
index 66c164200..af134caa1 100644
--- a/matita/contribs/CoRN-Decl/transc/Pi.ma
+++ b/matita/contribs/CoRN-Decl/transc/Pi.ma
@@ -16,12 +16,12 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/transc/Pi".
 
-include "CoRN_notation.ma".
+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