nasty change in the lexer/parser:

[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 97c1a9b6dfb67c738f0ed3addc7a8d0f30171ba0..87ec0e2dd289c9e58c7c08c5a01244c5d09d51d9 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/notation.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/notation.ma
@@ -14,3 +14,7 @@
 
 notation "hvbox (r \sub \c)"  with precedence 90 for @{'concr_rel $r}.
 notation "hvbox (r \sub \f)"  with precedence 90 for @{'form_rel $r}.
+
+definition hide ≝ λA:Type.λx:A.x.
+
+interpretation "hide" 'hide x = (hide ? x).