X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fnotation.ma;h=87ec0e2dd289c9e58c7c08c5a01244c5d09d51d9;hb=e78cf74f8976cf0ca554f64baa9979d0423ee927;hp=2cb92807d142ec9804e4eb98d8134c3a266e1012;hpb=ccac4e720ff2a9bee8e1c9d5ba1ea6474db72572;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/overlap/notation.ma b/helm/software/matita/contribs/formal_topology/overlap/notation.ma
index 2cb92807d..87ec0e2dd 100644
--- 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).