nasty change in the lexer/parser:

[helm.git] / helm / software / matita / contribs / POPLmark / Fsub / util.ma

diff --git a/helm/software/matita/contribs/POPLmark/Fsub/util.ma b/helm/software/matita/contribs/POPLmark/Fsub/util.ma
index ca2a0e730a767bae390868e3e72061e998e74048..d3f4dc02322141932af2c684ef8b65b476bfea63 100644 (file)
--- a/helm/software/matita/contribs/POPLmark/Fsub/util.ma
+++ b/helm/software/matita/contribs/POPLmark/Fsub/util.ma
@@ -49,7 +49,7 @@ notation > "hvbox(x ∈ l)"
 notation < "hvbox(x \nbsp ∈ \nbsp l)"
   non associative with precedence 30 for @{ 'inlist $x $l }.
 *)  
-interpretation "item in list" 'mem x l = (in_list _ x l).
+interpretation "item in list" 'mem x l = (in_list ? x l).
 
 lemma max_case : \forall m,n.(max m n) = match (leb m n) with
       [ true \Rightarrow n