- librarian: 3 bugs fixed in the building system:

[helm.git] / helm / software / matita / core_notation.moo

diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo
index b93dd98e1d79bfabcc629ae5aeeb1c62be894daf..be61e665096eb7f346ff55f4fae9f55fe54638c1 100644 (file)
--- 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