X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FGround_2%2Flist.ma;h=0a6e69bbee01308d429c242af9e17469b855b3c5;hb=ef3bdc4be26f6518a82a79c64e986253f7aeaa3c;hp=883a8a8baa7a8cc7eb899048e3c1fc00fb44534c;hpb=b5a168bec5e813258c510a1f2a00ce9f57ecee5a;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/Ground_2/list.ma b/matita/matita/contribs/lambda_delta/Ground_2/list.ma
index 883a8a8ba..0a6e69bbe 100644
--- a/matita/matita/contribs/lambda_delta/Ground_2/list.ma
+++ b/matita/matita/contribs/lambda_delta/Ground_2/list.ma
@@ -34,7 +34,7 @@ inductive list2 (A1,A2:Type[0]) : Type[0] :=
   | nil2 : list2 A1 A2
   | cons2: A1 → A2 → list2 A1 A2 → list2 A1 A2.
 
-interpretation "nil (list of pairs)" 'Nil2 = (nil2 ? ?). (**) (* 'Nil causes unification error in aacr_abst *)
+interpretation "nil (list of pairs)" 'Nil2 = (nil2 ? ?).
 
 interpretation "cons (list of pairs)" 'Cons hd1 hd2 tl = (cons2 ? ? hd1 hd2 tl).