X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FCSums.ma;h=3930cbf9febd05b374bad1b227d8fee8c85f6638;hb=7b05e20cb3ed6be79c2fdf94654047b1e58902f9;hp=b0fc1c6a256da0e1904891ecb350b9ea71a3a568;hpb=52206fa1c090fcdc8386ec8d7e88beca089c7e39;p=helm.git

diff --git a/matita/contribs/CoRN-Decl/algebra/CSums.ma b/matita/contribs/CoRN-Decl/algebra/CSums.ma
index b0fc1c6a2..3930cbf9f 100644
--- a/matita/contribs/CoRN-Decl/algebra/CSums.ma
+++ b/matita/contribs/CoRN-Decl/algebra/CSums.ma
@@ -39,10 +39,10 @@ include "algebra/CAbGroups.ma".
 *)
 
 (* UNEXPORTED
-Section Sums.
+Section Sums
 *)
 
-inline "cic:/CoRN/algebra/CSums/G.var".
+alias id "G" = "cic:/CoRN/algebra/CSums/Sums/G.var".
 
 (* Sum1 and Sum use subtraction *)
 
@@ -189,7 +189,7 @@ inline "cic:/CoRN/algebra/CSums/Sum_big_shift.con".
 inline "cic:/CoRN/algebra/CSums/Sumx_Sum0.con".
 
 (* UNEXPORTED
-End Sums.
+End Sums
 *)
 
 (* UNEXPORTED
@@ -216,10 +216,10 @@ often referred to as ``Mengolli Sums''.
 *)
 
 (* UNEXPORTED
-Section More_Sums.
+Section More_Sums
 *)
 
-inline "cic:/CoRN/algebra/CSums/G.var".
+alias id "G" = "cic:/CoRN/algebra/CSums/More_Sums/G.var".
 
 inline "cic:/CoRN/algebra/CSums/Mengolli_Sum.con".
 
@@ -230,7 +230,7 @@ inline "cic:/CoRN/algebra/CSums/str_Mengolli_Sum_gen.con".
 inline "cic:/CoRN/algebra/CSums/Sumx_to_Sum.con".
 
 (* UNEXPORTED
-End More_Sums.
+End More_Sums
 *)
 
 (* UNEXPORTED