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=45742b7c23599282cc2331692e329587640744ad;hpb=5e01cba364607e7937aec2e359c34f049bb0f108;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 45742b7c2..f97dfd9d0 100644
--- a/helm/software/matita/contribs/CoRN-Decl/algebra/ListType.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/algebra/ListType.ma
@@ -54,7 +54,7 @@ library of Coq but moved to the Type level.
 Section List
 *)
 
-inline "cic:/CoRN/algebra/ListType/List/A.var" "List__".
+alias id "A" = "cic:/CoRN/algebra/ListType/List/A.var".
 
 inline "cic:/CoRN/algebra/ListType/list.ind".
 
@@ -106,15 +106,15 @@ inline "cic:/CoRN/algebra/ListType/lel.con".
 Hint Unfold lel: list.
 *)
 
-inline "cic:/CoRN/algebra/ListType/List/length_order/a.var" "List__length_order__".
+alias id "a" = "cic:/CoRN/algebra/ListType/List/length_order/a.var".
 
-inline "cic:/CoRN/algebra/ListType/List/length_order/b.var" "List__length_order__".
+alias id "b" = "cic:/CoRN/algebra/ListType/List/length_order/b.var".
 
-inline "cic:/CoRN/algebra/ListType/List/length_order/l.var" "List__length_order__".
+alias id "l" = "cic:/CoRN/algebra/ListType/List/length_order/l.var".
 
-inline "cic:/CoRN/algebra/ListType/List/length_order/m.var" "List__length_order__".
+alias id "m" = "cic:/CoRN/algebra/ListType/List/length_order/m.var".
 
-inline "cic:/CoRN/algebra/ListType/List/length_order/n.var" "List__length_order__".
+alias id "n" = "cic:/CoRN/algebra/ListType/List/length_order/n.var".
 
 inline "cic:/CoRN/algebra/ListType/lel_refl.con".
 
@@ -223,11 +223,11 @@ Implicit Arguments cons [A].
 Section Map
 *)
 
-inline "cic:/CoRN/algebra/ListType/Map/A.var" "Map__".
+alias id "A" = "cic:/CoRN/algebra/ListType/Map/A.var".
 
-inline "cic:/CoRN/algebra/ListType/Map/B.var" "Map__".
+alias id "B" = "cic:/CoRN/algebra/ListType/Map/B.var".
 
-inline "cic:/CoRN/algebra/ListType/Map/f.var" "Map__".
+alias id "f" = "cic:/CoRN/algebra/ListType/Map/f.var".
 
 inline "cic:/CoRN/algebra/ListType/map.con".