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=f2d9db85559c7a8db11aae1153495fae4a258d54;hp=004ba5565748c06235c2dc3e9d6ca8fe646e8656;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;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 004ba5565..f97dfd9d0 100644
--- a/helm/software/matita/contribs/CoRN-Decl/algebra/ListType.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/algebra/ListType.ma
@@ -16,6 +16,8 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/algebra/ListType".
 
+include "CoRN.ma".
+
 (* begin hide *)
 
 (*#**********************************************************************)
@@ -48,41 +50,37 @@ This file contains a variant of the development of lists in the standard
 library of Coq but moved to the Type level.
 *)
 
-(* INCLUDE
-Le
-*)
-
 (* 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.
+inline "cic:/CoRN/algebra/ListType/list.ind".
 
-inline cic:/CoRN/algebra/ListType/app.con.
+inline "cic:/CoRN/algebra/ListType/app.con".
 
-inline cic:/CoRN/algebra/ListType/app_nil_end.con.
+inline "cic:/CoRN/algebra/ListType/app_nil_end.con".
 
 (* UNEXPORTED
 Hint Resolve app_nil_end: list v62.
 *)
 
-inline cic:/CoRN/algebra/ListType/app_ass.con.
+inline "cic:/CoRN/algebra/ListType/app_ass.con".
 
 (* UNEXPORTED
 Hint Resolve app_ass: list v62.
 *)
 
-inline cic:/CoRN/algebra/ListType/ass_app.con.
+inline "cic:/CoRN/algebra/ListType/ass_app.con".
 
 (* UNEXPORTED
 Hint Resolve ass_app: list v62.
 *)
 
-inline cic:/CoRN/algebra/ListType/tail.con.
+inline "cic:/CoRN/algebra/ListType/tail.con".
 
-inline cic:/CoRN/algebra/ListType/nil_cons.con.
+inline "cic:/CoRN/algebra/ListType/nil_cons.con".
 
 (*#***************************************)
 
@@ -90,7 +88,7 @@ inline cic:/CoRN/algebra/ListType/nil_cons.con.
 
 (*#***************************************)
 
-inline cic:/CoRN/algebra/ListType/length.con.
+inline "cic:/CoRN/algebra/ListType/length.con".
 
 (*#*****************************)
 
@@ -99,39 +97,39 @@ inline cic:/CoRN/algebra/ListType/length.con.
 (*#*****************************)
 
 (* UNEXPORTED
-Section length_order.
+Section length_order
 *)
 
-inline cic:/CoRN/algebra/ListType/lel.con.
+inline "cic:/CoRN/algebra/ListType/lel.con".
 
 (* UNEXPORTED
 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.
+inline "cic:/CoRN/algebra/ListType/lel_refl.con".
 
-inline cic:/CoRN/algebra/ListType/lel_trans.con.
+inline "cic:/CoRN/algebra/ListType/lel_trans.con".
 
-inline cic:/CoRN/algebra/ListType/lel_cons_cons.con.
+inline "cic:/CoRN/algebra/ListType/lel_cons_cons.con".
 
-inline cic:/CoRN/algebra/ListType/lel_cons.con.
+inline "cic:/CoRN/algebra/ListType/lel_cons.con".
 
-inline cic:/CoRN/algebra/ListType/lel_tail.con.
+inline "cic:/CoRN/algebra/ListType/lel_tail.con".
 
-inline cic:/CoRN/algebra/ListType/lel_nil.con.
+inline "cic:/CoRN/algebra/ListType/lel_nil.con".
 
 (* UNEXPORTED
-End length_order.
+End length_order
 *)
 
 (* UNEXPORTED
@@ -139,74 +137,74 @@ Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons: list
   v62.
 *)
 
-inline cic:/CoRN/algebra/ListType/In.con.
+inline "cic:/CoRN/algebra/ListType/In.con".
 
-inline cic:/CoRN/algebra/ListType/in_eq.con.
+inline "cic:/CoRN/algebra/ListType/in_eq.con".
 
 (* UNEXPORTED
 Hint Resolve in_eq: list v62.
 *)
 
-inline cic:/CoRN/algebra/ListType/in_cons.con.
+inline "cic:/CoRN/algebra/ListType/in_cons.con".
 
 (* UNEXPORTED
 Hint Resolve in_cons: list v62.
 *)
 
-inline cic:/CoRN/algebra/ListType/in_app_or.con.
+inline "cic:/CoRN/algebra/ListType/in_app_or.con".
 
 (* UNEXPORTED
 Hint Immediate in_app_or: list v62.
 *)
 
-inline cic:/CoRN/algebra/ListType/in_or_app.con.
+inline "cic:/CoRN/algebra/ListType/in_or_app.con".
 
 (* UNEXPORTED
 Hint Resolve in_or_app: list v62.
 *)
 
-inline cic:/CoRN/algebra/ListType/incl.con.
+inline "cic:/CoRN/algebra/ListType/incl.con".
 
 (* UNEXPORTED
 Hint Unfold incl: list v62.
 *)
 
-inline cic:/CoRN/algebra/ListType/incl_refl.con.
+inline "cic:/CoRN/algebra/ListType/incl_refl.con".
 
 (* UNEXPORTED
 Hint Resolve incl_refl: list v62.
 *)
 
-inline cic:/CoRN/algebra/ListType/incl_tl.con.
+inline "cic:/CoRN/algebra/ListType/incl_tl.con".
 
 (* UNEXPORTED
 Hint Immediate incl_tl: list v62.
 *)
 
-inline cic:/CoRN/algebra/ListType/incl_tran.con.
+inline "cic:/CoRN/algebra/ListType/incl_tran.con".
 
-inline cic:/CoRN/algebra/ListType/incl_appl.con.
+inline "cic:/CoRN/algebra/ListType/incl_appl.con".
 
 (* UNEXPORTED
 Hint Immediate incl_appl: list v62.
 *)
 
-inline cic:/CoRN/algebra/ListType/incl_appr.con.
+inline "cic:/CoRN/algebra/ListType/incl_appr.con".
 
 (* UNEXPORTED
 Hint Immediate incl_appr: list v62.
 *)
 
-inline cic:/CoRN/algebra/ListType/incl_cons.con.
+inline "cic:/CoRN/algebra/ListType/incl_cons.con".
 
 (* UNEXPORTED
 Hint Resolve incl_cons: list v62.
 *)
 
-inline cic:/CoRN/algebra/ListType/incl_app.con.
+inline "cic:/CoRN/algebra/ListType/incl_app.con".
 
 (* UNEXPORTED
-End List.
+End List
 *)
 
 (* UNEXPORTED
@@ -222,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.
+inline "cic:/CoRN/algebra/ListType/map.con".
 
 (* UNEXPORTED
-End Map.
+End Map
 *)
 
 (* UNEXPORTED