X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Ftransc%2FTrigonometric.ma;h=b4f59a9a8d9ac15ef229640ed9c1e5b8ce0b054d;hb=5e01cba364607e7937aec2e359c34f049bb0f108;hp=de100d31005b893a456483216b8b0b4bf7453b32;hpb=80110e17ef1d38d71473e9471ce15beddde663bb;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN-Decl/transc/Trigonometric.ma b/helm/software/matita/contribs/CoRN-Decl/transc/Trigonometric.ma
index de100d310..b4f59a9a8 100644
--- a/helm/software/matita/contribs/CoRN-Decl/transc/Trigonometric.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/transc/Trigonometric.ma
@@ -28,7 +28,7 @@ In this section, we explore the properties of the trigonometric functions which
 *)
 
 (* UNEXPORTED
-Section Lemmas.
+Section Lemmas
 *)
 
 (*#* First, we need a lemma on mappings. *)
@@ -36,11 +36,11 @@ Section Lemmas.
 inline "cic:/CoRN/transc/Trigonometric/maps_translation.con".
 
 (* UNEXPORTED
-End Lemmas.
+End Lemmas
 *)
 
 (* UNEXPORTED
-Section Sine_and_Cosine.
+Section Sine_and_Cosine
 *)
 
 (*#* Sine, cosine and tangent at [Zero]. *)
@@ -92,7 +92,7 @@ Hint Resolve Continuous_Sin Continuous_Cos: continuous.
 *)
 
 (* UNEXPORTED
-Section Sine_of_Sum.
+Section Sine_of_Sum
 *)
 
 (*#*
@@ -110,13 +110,13 @@ situations).
 
 (* begin hide *)
 
-inline "cic:/CoRN/transc/Trigonometric/F.con".
+inline "cic:/CoRN/transc/Trigonometric/Sine_and_Cosine/Sine_of_Sum/F.con" "Sine_and_Cosine__Sine_of_Sum__".
 
-inline "cic:/CoRN/transc/Trigonometric/G.con".
+inline "cic:/CoRN/transc/Trigonometric/Sine_and_Cosine/Sine_of_Sum/G.con" "Sine_and_Cosine__Sine_of_Sum__".
 
-inline "cic:/CoRN/transc/Trigonometric/F'.con".
+inline "cic:/CoRN/transc/Trigonometric/Sine_and_Cosine/Sine_of_Sum/F'.con" "Sine_and_Cosine__Sine_of_Sum__".
 
-inline "cic:/CoRN/transc/Trigonometric/G'.con".
+inline "cic:/CoRN/transc/Trigonometric/Sine_and_Cosine/Sine_of_Sum/G'.con" "Sine_and_Cosine__Sine_of_Sum__".
 
 (* end hide *)
 
@@ -201,7 +201,7 @@ inline "cic:/CoRN/transc/Trigonometric/Sin_plus_der_rht.con".
 inline "cic:/CoRN/transc/Trigonometric/Sin_plus_fun.con".
 
 (* UNEXPORTED
-End Sine_of_Sum.
+End Sine_of_Sum
 *)
 
 (* UNEXPORTED
@@ -211,6 +211,6 @@ Opaque Sine Cosine.
 inline "cic:/CoRN/transc/Trigonometric/Cos_plus_fun.con".
 
 (* UNEXPORTED
-End Sine_and_Cosine.
+End Sine_and_Cosine
 *)