From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 28 Jan 2009 09:11:42 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~4228
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ca5c21576ebd9a7bc9569cb8d713a9220392f2cf;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..b30eb2aba 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).