From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 9 Aug 2013 18:20:26 +0000 (+0000)
Subject: - the example is now minimal so the bug is understood.
X-Git-Tag: make_still_working~1111
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7ed62d94780c881c3ee056418b00ad5e9f739f15;p=helm.git

- the example is now minimal so the bug is understood.
  two interpretations of the same notation with the same description
  override eachother, so the description is not just informative :)
- more keywords added for highlighting
---

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/test.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/test.ma
index aac04467b..1f4fac570 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/test.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/test.ma
@@ -14,38 +14,26 @@
 
 universe constraint Type[0] < Type[1].
 
-(* notations ****************************************************************)
-
 notation "hvbox(a break \to b)"
   right associative with precedence 20
 for @{ \forall $_:$a.$b }.
 
-notation "hvbox( T . break ⓑ { term 46 I } break term 48 T1 )"
- non associative with precedence 47
- for @{ 'DxBind2 $T $I $T1 }.
-
-(* definitions **************************************************************)
-
-inductive lenv: Type[0] ≝
-| LAtom: lenv
-| LPair: lenv → lenv → lenv → lenv
-.
+notation "hvbox( * )"
+ non associative with precedence 90
+ for @{ 'B }.
 
-inductive genv: Type[0] ≝
-| GAtom: genv
-| GPair: genv → genv → genv → genv
-.
+inductive l: Type[0] ≝ L: l.
 
-axiom fw: genv → lenv → Prop.
+inductive g: Type[0] ≝ G: g.
 
-(* interpretations **********************************************************)
+axiom f: l → Prop.
 
-interpretation "environment binding construction (binary)"
-   'DxBind2 L I T = (LPair L I T).
+interpretation "b" 'B = L.
 
-interpretation "environment binding construction (binary)"
-   'DxBind2 G I T = (GPair G I T).
+interpretation "b" 'B = G.
 
-(* statements ***************************************************************)
+(* FG: two interpretations of the same notation and with the same description
+       override eachother, so the description is not just informative
+*)
 
-axiom fw_shift: ∀I,G,K,V. fw G (K.ⓑ{I}V).
+axiom s: f *.
diff --git a/matita/matita/matita.lang b/matita/matita/matita.lang
index 964ddeb1d..ea9d31828 100644
--- a/matita/matita/matita.lang
+++ b/matita/matita/matita.lang
@@ -109,6 +109,7 @@
           <keyword>alias</keyword>
           <keyword>and</keyword>
           <keyword>as</keyword>
+          <keyword>associative</keyword>
           <keyword>coercion</keyword>
           <keyword>prefer</keyword>
           <keyword>nocomposites</keyword>
@@ -124,15 +125,19 @@
           <keyword>inverter</keyword>
           <keyword>in</keyword>
           <keyword>interpretation</keyword>
+	  <keyword>left</keyword>          
           <keyword>let</keyword>
           <keyword>match</keyword>
           <keyword>names</keyword>
-          <keyword>notation</keyword>
+	  <keyword>non</keyword>          
+	  <keyword>notation</keyword>
           <keyword>on</keyword>
+          <keyword>precedence</keyword>
           <keyword>qed</keyword>
           <keyword>rec</keyword>
           <keyword>record</keyword>
           <keyword>return</keyword>
+	  <keyword>right</keyword>          
           <keyword>source</keyword>    
           <keyword>to</keyword>
           <keyword>universe</keyword>