X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Fbasics%2Flist.ma;h=d6c0661208c15e31c7b10684657a3f98bbd0060c;hb=b503649d75bd4cb8edf87418abfd56bf06c18cfd;hp=4e44ce298396d089a0fb97543c26cf94b770fa1e;hpb=e593e93ca00c6e9dfb8f0e79cb52684c5b104c3f;p=helm.git

diff --git a/weblib/basics/list.ma b/weblib/basics/list.ma
index 4e44ce298..d6c066120 100644
--- a/weblib/basics/list.ma
+++ b/weblib/basics/list.ma
@@ -9,7 +9,7 @@
      \ /   GNU General Public License Version 2   
       V_______________________________________________________________ *)
 
-include "arithmetics/nat.ma".span class="error" title="disambiguation error"/span
+include "arithmetics/nat.ma".
 
 inductive list (A:Type[0]) : Type[0] :=
   | nil: list A
@@ -237,4 +237,4 @@ theorem fold_sum: ∀A,B. ∀I,J:a href="cic:/matita/basics/list/list.ind(1,0,1
     a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i∈(Ia title="append" href="cic:/fakeuri.def(1)"@/aJ)} (f i).
 #A #B #I #J #nil #op #f (elim I) normalize 
   [>a href="cic:/matita/basics/list/nill.fix(0,2,2)"nill/a //|#a #tl #Hind <a href="cic:/matita/basics/list/assoc.fix(0,2,2)"assoc/a //]
-qed.
\ No newline at end of file
+qed.