additions to Basic_2

[helm.git] / matita / matita / contribs / lambda_delta / Ground_2 / list.ma

diff --git a/matita/matita/contribs/lambda_delta/Ground_2/list.ma b/matita/matita/contribs/lambda_delta/Ground_2/list.ma
index 883a8a8baa7a8cc7eb899048e3c1fc00fb44534c..0a6e69bbee01308d429c242af9e17469b855b3c5 100644 (file)
--- 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).