X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Flist%2Flist.ma;h=c6fd212beca5b6f8b623b39cf95bee3508c48fac;hb=442f3a15d7c6afc480da02602d4d4c8db4f44c10;hp=d0c4f58563005e638aafde095019b2663f78dbad;hpb=4dc47c9675ffd5fa50296ffaa9b5997501518c98;p=helm.git

diff --git a/helm/software/matita/library/list/list.ma b/helm/software/matita/library/list/list.ma
index d0c4f5856..c6fd212be 100644
--- a/helm/software/matita/library/list/list.ma
+++ b/helm/software/matita/library/list/list.ma
@@ -34,8 +34,8 @@ notation "hvbox(l1 break @ l2)"
   right associative with precedence 47
   for @{'append $l1 $l2 }.
 
-interpretation "nil" 'nil = (nil _).
-interpretation "cons" 'cons hd tl = (cons _ hd tl).
+interpretation "nil" 'nil = (nil ?).
+interpretation "cons" 'cons hd tl = (cons ? hd tl).
 
 (* theorem test_notation: [O; S O; S (S O)] = O :: S O :: S (S O) :: []. *)
 
@@ -62,7 +62,7 @@ definition tail := \lambda A:Type. \lambda l: list A.
   [ nil => []
   | (cons hd tl) => tl].
 
-interpretation "append" 'append l1 l2 = (append _ l1 l2).
+interpretation "append" 'append l1 l2 = (append ? l1 l2).
 
 theorem append_nil: \forall A:Type.\forall l:list A.l @ [] = l.
   intros;