...

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / notation.ma

diff --git a/helm/software/matita/contribs/formal_topology/overlap/notation.ma b/helm/software/matita/contribs/formal_topology/overlap/notation.ma
index 2cb92807d142ec9804e4eb98d8134c3a266e1012..b30eb2aba564ce645f4b8c95b211d8b9717f6e21 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/notation.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/notation.ma
@@ -15,9 +15,6 @@
 notation "hvbox (r \sub \c)"  with precedence 90 for @{'concr_rel $r}.
 notation "hvbox (r \sub \f)"  with precedence 90 for @{'form_rel $r}.
 
-notation < "mstyle color #ff0000 (…)" non associative with precedence 90
-for @{'hide}.
-
 definition hide ≝ λA:Type.λx:A.x.
 
-interpretation "hide" 'hide = (hide _ _). 
+interpretation "hide" 'hide x = (hide _ x).