X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Freals%2FRealLists.ma;h=322b20456a5f610dec622d048cb5cb0415a20b76;hb=b4670008138505f7462252c29eb755ab127862ba;hp=26b92efdfcf99465e9cc79a76a29749a553ba09e;hpb=7a8f91f8aa2d6ba24bf6b3093866f759ee16e690;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN-Decl/reals/RealLists.ma b/helm/software/matita/contribs/CoRN-Decl/reals/RealLists.ma
index 26b92efdf..322b20456 100644
--- a/helm/software/matita/contribs/CoRN-Decl/reals/RealLists.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/reals/RealLists.ma
@@ -16,14 +16,14 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/reals/RealLists".
 
-include "CoRN_notation.ma".
+include "CoRN.ma".
 
 (* $Id: RealLists.v,v 1.4 2004/04/23 10:01:05 lcf Exp $ *)
 
 include "reals/CReals1.ma".
 
 (* UNEXPORTED
-Section Lists.
+Section Lists
 *)
 
 (*#* * Lists of Real Numbers
@@ -76,7 +76,7 @@ inline "cic:/CoRN/reals/RealLists/maxlist_greater.con".
 
 (* begin hide *)
 
-inline "cic:/CoRN/reals/RealLists/maxlist_aux.con".
+inline "cic:/CoRN/reals/RealLists/Lists/maxlist_aux.con" "Lists__".
 
 (* end hide *)
 
@@ -90,7 +90,7 @@ inline "cic:/CoRN/reals/RealLists/minlist_smaller.con".
 
 (* begin hide *)
 
-inline "cic:/CoRN/reals/RealLists/minlist_aux.con".
+inline "cic:/CoRN/reals/RealLists/Lists/minlist_aux.con" "Lists__".
 
 (* end hide *)
 
@@ -101,6 +101,6 @@ inline "cic:/CoRN/reals/RealLists/less_minlist.con".
 inline "cic:/CoRN/reals/RealLists/leEq_minlist.con".
 
 (* UNEXPORTED
-End Lists.
+End Lists
 *)