X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Ftransc%2FSinCos.ma;h=314d0f5fa686496b7232784a91871434ce2fd2eb;hb=16d0ba4a14fd6bede3e8b3520af7deaefb4f8068;hp=f302c538dd172ba44f6b1d73e56037fd3eeb408b;hpb=7a8f91f8aa2d6ba24bf6b3093866f759ee16e690;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN-Decl/transc/SinCos.ma b/helm/software/matita/contribs/CoRN-Decl/transc/SinCos.ma
index f302c538d..314d0f5fa 100644
--- a/helm/software/matita/contribs/CoRN-Decl/transc/SinCos.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/transc/SinCos.ma
@@ -16,14 +16,14 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/transc/SinCos".
 
-include "CoRN_notation.ma".
+include "CoRN.ma".
 
 (* $Id: SinCos.v,v 1.6 2004/04/23 10:01:08 lcf Exp $ *)
 
 include "transc/Trigonometric.ma".
 
 (* UNEXPORTED
-Section Sum_and_so_on.
+Section Sum_and_so_on
 *)
 
 (* UNEXPORTED
@@ -32,13 +32,13 @@ Opaque Sine Cosine.
 
 (* begin hide *)
 
-inline "cic:/CoRN/transc/SinCos/F.con".
+inline "cic:/CoRN/transc/SinCos/Sum_and_so_on/F.con" "Sum_and_so_on__".
 
-inline "cic:/CoRN/transc/SinCos/G.con".
+inline "cic:/CoRN/transc/SinCos/Sum_and_so_on/G.con" "Sum_and_so_on__".
 
-inline "cic:/CoRN/transc/SinCos/F'.con".
+inline "cic:/CoRN/transc/SinCos/Sum_and_so_on/F'.con" "Sum_and_so_on__".
 
-inline "cic:/CoRN/transc/SinCos/G'.con".
+inline "cic:/CoRN/transc/SinCos/Sum_and_so_on/G'.con" "Sum_and_so_on__".
 
 (* end hide *)
 
@@ -103,7 +103,7 @@ Hint Resolve FFT: algebra.
 inline "cic:/CoRN/transc/SinCos/FFT'.con".
 
 (* UNEXPORTED
-End Sum_and_so_on.
+End Sum_and_so_on
 *)
 
 (* UNEXPORTED
@@ -124,7 +124,7 @@ Opaque Min Sine Cosine.
 *)
 
 (* UNEXPORTED
-Section Basic_Properties.
+Section Basic_Properties
 *)
 
 (*#* **Basic properties
@@ -167,7 +167,7 @@ inline "cic:/CoRN/transc/SinCos/Sin_less_One.con".
 inline "cic:/CoRN/transc/SinCos/AbsIR_Sin_less_One.con".
 
 (* UNEXPORTED
-End Basic_Properties.
+End Basic_Properties
 *)
 
 (* UNEXPORTED