- 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 aac04467bace657625aa5f1eb8ed62bbd6c8552c..1f4fac570da00244a59ed15e141889837735c4e1 100644 (file)
--- 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 964ddeb1d5c5c04134294ad4ab1997804bf24aca..ea9d318283a14d42ab5ff3283a1eb899815ef7db 100644 (file)
--- 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>