X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcore_notation.moo;h=be61e665096eb7f346ff55f4fae9f55fe54638c1;hb=68dbcd02022874a025a9444aa1125b0458816fbb;hp=b93dd98e1d79bfabcc629ae5aeeb1c62be894daf;hpb=1e1f24496beba354fb3f550496858b5755d9be0b;p=helm.git

diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo
index b93dd98e1..be61e6650 100644
--- a/helm/software/matita/core_notation.moo
+++ b/helm/software/matita/core_notation.moo
@@ -1,5 +1,9 @@
 (* exists *******************************************************************)
 
+notation "hvbox(∃ _ break . p)"
+ with precedence 20
+for @{'exists $p }.
+
 notation < "hvbox(\exists ident i : ty break . p)"
  right associative with precedence 20
 for @{'exists (\lambda ${ident i} : $ty. $p) }.
@@ -8,10 +12,6 @@ notation < "hvbox(\exists ident i break . p)"
   with precedence 20
 for @{'exists (\lambda ${ident i}. $p) }.
 
-notation "hvbox(∃ _ break . p)"
- with precedence 20
-for @{'exists $p }.
-
 (*
 notation < "hvbox(\exists ident i opt (: ty) break . p)"
   right associative with precedence 20