X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FListType.ma;h=f97dfd9d044be0294313d0f34a657bb451d31eee;hb=bf0cc84dcef9ae3d2145e79754bb39feb3985574;hp=b4a8978be8456761a36fc8d341e094aa710143f8;hpb=7a8f91f8aa2d6ba24bf6b3093866f759ee16e690;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/ListType.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/ListType.ma
index b4a8978be..f97dfd9d0 100644
--- a/helm/software/matita/contribs/CoRN-Decl/algebra/ListType.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/algebra/ListType.ma
@@ -16,7 +16,7 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/algebra/ListType".
 
-include "CoRN_notation.ma".
+include "CoRN.ma".
 
 (* begin hide *)
 
@@ -51,10 +51,10 @@ library of Coq but moved to the Type level.
 *)
 
 (* UNEXPORTED
-Section List.
+Section List
 *)
 
-inline "cic:/CoRN/algebra/ListType/A.var".
+alias id "A" = "cic:/CoRN/algebra/ListType/List/A.var".
 
 inline "cic:/CoRN/algebra/ListType/list.ind".
 
@@ -97,7 +97,7 @@ inline "cic:/CoRN/algebra/ListType/length.con".
 (*#*****************************)
 
 (* UNEXPORTED
-Section length_order.
+Section length_order
 *)
 
 inline "cic:/CoRN/algebra/ListType/lel.con".
@@ -106,15 +106,15 @@ inline "cic:/CoRN/algebra/ListType/lel.con".
 Hint Unfold lel: list.
 *)
 
-inline "cic:/CoRN/algebra/ListType/a.var".
+alias id "a" = "cic:/CoRN/algebra/ListType/List/length_order/a.var".
 
-inline "cic:/CoRN/algebra/ListType/b.var".
+alias id "b" = "cic:/CoRN/algebra/ListType/List/length_order/b.var".
 
-inline "cic:/CoRN/algebra/ListType/l.var".
+alias id "l" = "cic:/CoRN/algebra/ListType/List/length_order/l.var".
 
-inline "cic:/CoRN/algebra/ListType/m.var".
+alias id "m" = "cic:/CoRN/algebra/ListType/List/length_order/m.var".
 
-inline "cic:/CoRN/algebra/ListType/n.var".
+alias id "n" = "cic:/CoRN/algebra/ListType/List/length_order/n.var".
 
 inline "cic:/CoRN/algebra/ListType/lel_refl.con".
 
@@ -129,7 +129,7 @@ inline "cic:/CoRN/algebra/ListType/lel_tail.con".
 inline "cic:/CoRN/algebra/ListType/lel_nil.con".
 
 (* UNEXPORTED
-End length_order.
+End length_order
 *)
 
 (* UNEXPORTED
@@ -204,7 +204,7 @@ Hint Resolve incl_cons: list v62.
 inline "cic:/CoRN/algebra/ListType/incl_app.con".
 
 (* UNEXPORTED
-End List.
+End List
 *)
 
 (* UNEXPORTED
@@ -220,19 +220,19 @@ Implicit Arguments cons [A].
 *)
 
 (* UNEXPORTED
-Section Map.
+Section Map
 *)
 
-inline "cic:/CoRN/algebra/ListType/A.var".
+alias id "A" = "cic:/CoRN/algebra/ListType/Map/A.var".
 
-inline "cic:/CoRN/algebra/ListType/B.var".
+alias id "B" = "cic:/CoRN/algebra/ListType/Map/B.var".
 
-inline "cic:/CoRN/algebra/ListType/f.var".
+alias id "f" = "cic:/CoRN/algebra/ListType/Map/f.var".
 
 inline "cic:/CoRN/algebra/ListType/map.con".
 
 (* UNEXPORTED
-End Map.
+End Map
 *)
 
 (* UNEXPORTED