- new library/logic/coimplication.ma uses new decompose tactic

[helm.git] / helm / software / matita / contribs / CoRN-Decl / algebra / CSums.ma

diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/CSums.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/CSums.ma
index 133a29096b8cf1e382ffb1ee6b979e3c4f58d540..c90312746f3ca716307189216a9b55c439db2455 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Decl/algebra/CSums.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/algebra/CSums.ma
@@ -16,7 +16,7 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/algebra/CSums".
 
-include "CoRN_notation.ma".
+include "CoRN.ma".
 
 (* $Id: CSums.v,v 1.8 2004/04/23 10:00:54 lcf Exp $ *)
 
@@ -39,10 +39,10 @@ include "algebra/CAbGroups.ma".
 *)
 
 (* UNEXPORTED
-Section Sums.
+Section Sums
 *)
 
-inline "cic:/CoRN/algebra/CSums/G.var".
+inline "cic:/CoRN/algebra/CSums/Sums/G.var" "Sums__".
 
 (* 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".
+inline "cic:/CoRN/algebra/CSums/More_Sums/G.var" "More_Sums__".
 
 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