Parsing des motifs de Syntax avec la grammaire associée à l'univers de la déclaration (constr, tactic ou vernac) au lieu de ast (comme cela a été fait pour Grammar)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@721 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 102 insertions, 101 deletions

diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v
index 57b76e0176..06aa131023 100644
--- a/theories/Init/LogicSyntax.v
+++ b/theories/Init/LogicSyntax.v
@@ -51,42 +51,42 @@ with constr10 :=
 
 Syntax constr
   level 1:
-    equal [<<(eq $_  $t1  $t2)>>] -> [ [<hov 0> $t1:E [0 1]  "=" $t2:E ] ]
-  | conj [<<(conj $t1 $t2 $t3 $t4)>>]
+    equal [ (eq $_  $t1  $t2) ] -> [ [<hov 0> $t1:E [0 1]  "=" $t2:E ] ]
+  | conj [ (conj $t1 $t2 $t3 $t4) ]
       -> [ [<hov 1> [<hov 1> "<" $t1:L "," [0 0] $t2:L ">" ] [0 0]
                     [<hov 1> "{" $t3:L "," [0 0] $t4:L "}"] ] ]
-  | IF [<< either $c and_then $t or_else $e >>]
+  | IF [ either $c and_then $t or_else $e ]
       -> [ [<hov 0> "either" [1 1] $c:E
                 [<hov 0> [1 1] "and_then" [1 1] $t:E ]
                 [<hov 0> [1 1] "or_else" [1 1] $e:E ]] ]
   ;
 
   level 2:
-    not [<< ~ $t1 >>] -> [ [<hov 0> "~" $t1:E ] ]
+    not [ ~ $t1 ] -> [ [<hov 0> "~" $t1:E ] ]
   ;
 
   level 6:
-    and [<< $t1 /\ $t2 >>] -> [ [<hov 0> $t1:L [0 0] "/\\" $t2:E ] ]
+    and [ $t1 /\ $t2 ] -> [ [<hov 0> $t1:L [0 0] "/\\" $t2:E ] ]
   ;
 
   level 7:
-    or [<< $t1 \/ $t2 >>] -> [ [<hov 0> $t1:L [0 0]  "\\/" $t2:E ] ]
+    or [ $t1 \/ $t2 ] -> [ [<hov 0> $t1:L [0 0]  "\\/" $t2:E ] ]
   ;
 
   level 8:
-    iff [<< $t1 <-> $t2 >>] -> [ [<hov 0> $t1:L [0 0] "<->" $t2:E ] ]
+    iff [ $t1 <-> $t2 ] -> [ [<hov 0> $t1:L [0 0] "<->" $t2:E ] ]
   ;
 
   level 10:
-    all_pred [<<(all $_ $p)>>] -> [ [<hov 4> "All " $p:L ] ]
-  | all_imp [<<(all $_ [$x : $T]$t)>>]
+    all_pred [ (all $_ $p) ] -> [ [<hov 4> "All " $p:L ] ]
+  | all_imp [ (all $_ [$x : $T]$t) ]
        -> [ [<hov 3> "ALL " $x ":" $T:L " |" [1 0] $t:L ] ]
 
-  | ex_pred [<<(ex $_ $p)>>] -> [ [<hov 0> "Ex " $p:L ] ]
-  | ex [<<(ex $_ [$x : $T]$P)>>] 
+  | ex_pred [ (ex $_ $p) ] -> [ [<hov 0> "Ex " $p:L ] ]
+  | ex [ (ex $_ [$x : $T]$P) ] 
        -> [ [<hov 2> "EX " $x ":" $T:L " |" [1 0] $P:L ] ]
 
-  | ex2_pred [<<(ex2 $_ $p1 $p2)>>]
+  | ex2_pred [ (ex2 $_ $p1 $p2) ]
        -> [ [<hov 3> "Ex2 " $p1:L [1 0] $p2:L ] ]
-  | ex2 [<<(ex2 $_ [$x : T]$P1 [$x : $T]$P2)>>] 
+  | ex2 [ (ex2 $_ [$x : T]$P1 [$x : $T]$P2) ] 
        -> [ [<hov 2> "EX " $x ":" $T:L " |" [1 2] $P1:L [1 0] "& " $P2:L] ].
diff --git a/theories/Init/Logic_TypeSyntax.v b/theories/Init/Logic_TypeSyntax.v
index 6760bcafa6..5064ddcec8 100644
--- a/theories/Init/Logic_TypeSyntax.v
+++ b/theories/Init/Logic_TypeSyntax.v
@@ -31,22 +31,22 @@ with command10 :=
 
 Syntax constr
   level 10:
-    allT_pred [<<(allT $_ $p)>>] -> [ [<hov 0> "AllT " $p:L ] ]
-  | allT [<<(allT $T [$x : $T]$p)>>]
+    allT_pred [ (allT $_ $p) ] -> [ [<hov 0> "AllT " $p:L ] ]
+  | allT [ (allT $T [$x : $T]$p) ]
        -> [ [<hov 3> "ALLT " $x ":" $T:L " |" [1 0] $p:L ] ]
 
-  | exT_pred [<<(exT $_ $p)>>] -> [ [<hov 4> "ExT " $p:L ] ]
-  | exT [<<(exT $t1 [$x : $T]$p)>>] 
+  | exT_pred [ (exT $_ $p) ] -> [ [<hov 4> "ExT " $p:L ] ]
+  | exT [ (exT $t1 [$x : $T]$p) ] 
        -> [ [<hov 4> "EXT " $x ":" $T:L " |" [1 0] $p:L ] ]
 
-  | exT2_pred [<<(exT2 $_ $p1 $p2)>>]
+  | exT2_pred [ (exT2 $_ $p1 $p2) ]
        -> [ [<hov 4> "ExT2 " $p1:L [1 0] $p2:L ] ]
-  | exT2 [<<(exT2 $T [$x : $T]$P1 [$x : $T]$P2)>>] 
+  | exT2 [ (exT2 $T [$x : $T]$P1 [$x : $T]$P2) ] 
        -> [ [<hov 2> "EXT " $x ":" $T:L " |" [1 2] $P1:L [1 0] "& " $P2:L] ]
   ;
 
   level 1:
-    eqT [<<(eqT $_ $c1 $c2)>>] -> [ [<hov 1> $c1:E [0 0] "==" $c2:E ] ]
+    eqT [ (eqT $_ $c1 $c2) ] -> [ [<hov 1> $c1:E [0 0] "==" $c2:E ] ]
 
-  | identityT [<<(identityT $_ $c1 $c2)>>]
+  | identityT [ (identityT $_ $c1 $c2) ]
        -> [ [<hov 1> $c1:E [0 0] "===" $c2:E ] ].
diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v
index a3a69c3100..33f5fad72a 100644
--- a/theories/Init/SpecifSyntax.v
+++ b/theories/Init/SpecifSyntax.v
@@ -42,85 +42,86 @@ Syntax constr
   (* Default pretty-printing rules *)
   level 10:
     sig_var
-      [(ABSTR_B_NB $c1 $c2)] -> [ [<hov 0> "sig " $c1:L [1 1] $c2:L ] ]
+      [<<(ABSTR_B_NB $c1 $c2)>>] -> [ [<hov 0> "sig " $c1:L [1 1] $c2:L ] ]
   | sig2_var
-      [(Sig2_ABSTR_B_NB $c1 $c2)] -> [ [<hov 0> "sig2 " $c1:L [1 1] $c2:L ] ]
+      [<<(Sig2_ABSTR_B_NB $c1 $c2)>>] -> [ [<hov 0> "sig2 " $c1:L [1 1] $c2:L ] ]
   | sigS_var
-      [(SigS_ABSTR_B_NB $c1 $c2)] -> [ [<hov 0> "sigS " $c1:L [1 1] $c2:L ] ]
-  | sigS2_var [(SigS2_ABSTR_B_NB $c1 $c2 $c3)]
+      [<<(SigS_ABSTR_B_NB $c1 $c2)>>] -> [ [<hov 0> "sigS " $c1:L [1 1] $c2:L ] ]
+  | sigS2_var [<<(SigS2_ABSTR_B_NB $c1 $c2 $c3)>>]
       -> [ [<hov 0> "sigS2 " $c1:L [1 1] $c2:L [1 1] $c3:L] ]
   ;
 
   level 1:
 (* Pretty-printing of [sig] *)
-    sig  [<<(sig $c1 $c2)>>] -> [ (ABSTR_B_NB  $c1 $c2):E ]
-  | sig_nb [(ABSTR_B_NB $c1 (LAMBDALIST $c1 [<>]$c2))]
+    sig  [ (sig $c1 $c2) ] -> [ (ABSTR_B_NB  $c1 $c2):E ]
+  | sig_nb [ << (ABSTR_B_NB $c1 (LAMBDALIST $c1 [<>]$c2)) >> ]
       -> [ [<hov 0> "{_:" $c1:E " |" [1 3] $c2:E "}" ] ]
-  | sigma_b [(ABSTR_B_NB $c1 (LAMBDALIST $c1 [$id]$c2))]
+  | sigma_b [ << (ABSTR_B_NB $c1 (LAMBDALIST $c1 [$id]$c2)) >> ]
       -> [ [<hov 0> "{" $id ":" $c1:E " |" [1 3] $c2:E "}" ] ]
 
 (* Pretty-printing of [sig2] *)
-  | sig2 [<<(sig2 $c1 $c2 $c3)>>] -> [ (Sig2_ABSTR_B_NB  $c1 $c2 $c3):E ]
+  | sig2 [ (sig2 $c1 $c2 $c3) ] -> [ (Sig2_ABSTR_B_NB  $c1 $c2 $c3):E ]
   | sig2_b_b
-      [(Sig2_ABSTR_B_NB $c1 (LAMBDALIST $c1 [$id]$c2)
-                            (LAMBDALIST $c1 [$id]$c3))]
+      [ << (Sig2_ABSTR_B_NB $c1 (LAMBDALIST $c1 [$id]$c2)
+                            (LAMBDALIST $c1 [$id]$c3)) >> ]
        -> [ [<hov 0> "{"$id":"$c1:E"|" [1 3]$c2:E [1 3]"& "$c3:E "}" ] ]
   | sig2_nb_b
-      [(Sig2_ABSTR_B_NB $c1 (LAMBDALIST $c1 [<>]$c2)
-                            (LAMBDALIST  $c1 [$id]$c3))]
+      [ << (Sig2_ABSTR_B_NB $c1 (LAMBDALIST $c1 [<>]$c2)
+                            (LAMBDALIST  $c1 [$id]$c3)) >> ]
        -> [ [<hov 0> "{"$id":"$c1:E"|" [1 3]$c2:E [1 3]"& "$c3:E "}" ] ]
   | sig2_b_nb
-      [(Sig2_ABSTR_B_NB $c1 (LAMBDALIST $c1 [$id]$c2)
-                            (LAMBDALIST $c1 [<>]$c3))]
+      [ << (Sig2_ABSTR_B_NB $c1 (LAMBDALIST $c1 [$id]$c2)
+                            (LAMBDALIST $c1 [<>]$c3)) >> ]
        -> [ [<hov 0> "{"$id":"$c1:E"|" [1 3]$c2:E [1 3]"& "$c3:E "}" ] ]
   | sig2_nb_nb
-      [(Sig2_ABSTR_B_NB $c1 (LAMBDALIST $c1 [<>]$c2)
-                            (LAMBDALIST $c1 [<>]$c3))]
+      [ << (Sig2_ABSTR_B_NB $c1 (LAMBDALIST $c1 [<>]$c2)
+                            (LAMBDALIST $c1 [<>]$c3)) >> ]
        -> [ [<hov 0> "{_:"$c1:E "|" [1 3] $c2:E [1 3]"& " $c3:E "}" ] ]
 
 (* Pretty-printing of [sigS] *)
-  | sigS [<<(sigS $c1 $c2)>>] -> [(SigS_ABSTR_B_NB  $c1 $c2):E]
-  | sigS_nb [(SigS_ABSTR_B_NB $c1 (LAMBDALIST $c1 [<>]$c2))]
+  | sigS [ (sigS $c1 $c2) ] -> [(SigS_ABSTR_B_NB  $c1 $c2):E]
+  | sigS_nb [ << (SigS_ABSTR_B_NB $c1 (LAMBDALIST $c1 [<>]$c2)) >> ]
        -> [ [<hov 0> "{_:" $c1:E [1 3]"& " $c2:E  "}" ] ]
-  | sigS_b [(SigS_ABSTR_B_NB $c1 (LAMBDALIST $c1 [$id]$c2))]
+  | sigS_b [ << (SigS_ABSTR_B_NB $c1 (LAMBDALIST $c1 [$id]$c2)) >> ]
        -> [ [<hov 0> "{" $id  ":" $c1:E [1 3] "& " $c2:E "}" ] ]
 
 (* Pretty-printing of [sigS2] *)
-  | sigS2 [<<(sigS2 $c1 $c2 $c3)>>] -> [(SigS2_ABSTR_B_NB  $c1 $c2 $c3):E]
+  | sigS2 [ (sigS2 $c1 $c2 $c3) ] -> [(SigS2_ABSTR_B_NB  $c1 $c2 $c3):E]
   | sigS2_b_b
-      [(SigS2_ABSTR_B_NB $c1 (LAMBDALIST $c1 [$id]$c2)
-                             (LAMBDALIST $c1 [$id]$c3))]
+      [ << (SigS2_ABSTR_B_NB $c1 (LAMBDALIST $c1 [$id]$c2)
+                             (LAMBDALIST $c1 [$id]$c3)) >> ]
        -> [ [<hov 0> "{"$id ":" $c1:E [1 3]"& "$c2:E [1 3]"& "$c3:E "}" ] ]
   | sigS2_nb_b
-      [(SigS2_ABSTR_B_NB $c1 (LAMBDALIST $c1 [<>]$c2)
-                             (LAMBDALIST  $c1 [$id]$c3))]
+      [ << (SigS2_ABSTR_B_NB $c1 (LAMBDALIST $c1 [<>]$c2)
+                             (LAMBDALIST  $c1 [$id]$c3)) >> ]
        -> [ [<hov 0> "{"$id ":" $c1:E [1 3]"& "$c2:E [1 3]"& "$c3:E "}" ] ]
   | sigS2_b_nb
-      [ (SigS2_ABSTR_B_NB $c1 (LAMBDALIST $c1 [$id]$c2)
-                              (LAMBDALIST $c1 [<>]$c3))]
+      [ << (SigS2_ABSTR_B_NB $c1 (LAMBDALIST $c1 [$id]$c2)
+                              (LAMBDALIST $c1 [<>]$c3)) >> ]
        -> [ [<hov 0> "{"$id ":" $c1:E [1 3]"& "$c2:E [1 3]"& "$c3:E "}" ] ]
   | sigS2_nb_nb
-      [(SigS2_ABSTR_B_NB $c1 (LAMBDALIST $c1 [<>]$c2)
-                             (LAMBDALIST $c1 [<>]$c3))]
+      [ << (SigS2_ABSTR_B_NB $c1 (LAMBDALIST $c1 [<>]$c2)
+                             (LAMBDALIST $c1 [<>]$c3)) >> ]
        -> [ [<hov 0> "{_:"$c1:E [1 3]"& "$c2:E [1 3]"& "$c3:E "}" ] ]
 
 (* Pretty-printing of [projS1] and [projS2] *)
-  | projS1_imp [<<(projS1 ? ? $a)>>] -> ["(ProjS1 " $a:E ")"]  
-  | projS2_imp [<<(projS2 ? ? $a)>>] -> ["(ProjS2 " $a:E ")"]
+  | projS1_imp [ (projS1 ? ? $a) ] -> ["(ProjS1 " $a:E ")"]  
+  | projS2_imp [ (projS2 ? ? $a) ] -> ["(ProjS2 " $a:E ")"]
   ;
 
 (* Pretty-printing of [sumbool] and [sumor] *)
   level 4:
-    sumbool [<<(sumbool $t1 $t2)>>]
+    sumbool [ (sumbool $t1 $t2) ]
        -> [ [<hov 0> "{" $t1:E "}" [0 1] "+" "{" $t2:L "}"] ]
-  | sumor [<<(sumor $t1 $t2)>>]
+  | sumor [ (sumor $t1 $t2) ]
        -> [ [<hov 0> $t1:E [0 1]  "+" "{" $t2:L "}"] ]
   ;
 
 (* Pretty-printing of [except] *)
   level 1:
-    Except_imp [<<(except $1 $t2)>>] -> [ [<hov 0> "Except " $t2 ] ]
+    Except_imp [ (except $1 $t2) ] -> [ [<hov 0> "Except " $t2 ] ]
 
 (* Pretty-printing of [error] and [value] *)
-  | Error_imp [<<(error $t1)>>]     -> [ [<hov 0> "Error" ] ]
-  | Value_imp [<<(value $t1 $t2)>>] -> [ [<hov 0> "(Value " $t2 ")" ] ].
+  | Error_imp [ (error $t1) ]     -> [ [<hov 0> "Error" ] ]
+  | Value_imp [ (value $t1 $t2) ] -> [ [<hov 0> "(Value " $t2 ")" ] ].
+
diff --git a/theories/Zarith/Zsyntax.v b/theories/Zarith/Zsyntax.v
index 350bcaa180..df7551e6ab 100644
--- a/theories/Zarith/Zsyntax.v
+++ b/theories/Zarith/Zsyntax.v
@@ -85,125 +85,125 @@ Grammar command atomic_pattern :=
 
 Syntax constr
   level 0:
-    My_special_variable0 [<< My_special_variable0 >>] -> [ "POS" ]
-  | My_special_variable1 [<< My_special_variable1 >>] -> [ "NEG" ] 
-  | Zle [<<(Zle $n1 $n2)>>] -> 
+    My_special_variable0 [ My_special_variable0 ] -> [ "POS" ]
+  | My_special_variable1 [ My_special_variable1 ] -> [ "NEG" ] 
+  | Zle [ (Zle $n1 $n2) ] -> 
       [[<hov 0> "`" (ZEXPR $n1) [1 0] "<= " (ZEXPR $n2) "`"]]
-  | Zlt [<<(Zlt $n1 $n2)>>] -> 
+  | Zlt [ (Zlt $n1 $n2) ] -> 
       [[<hov 0> "`" (ZEXPR $n1) [1 0] "< "(ZEXPR $n2) "`" ]]
-  | Zge [<<(Zge $n1 $n2)>>] -> 
+  | Zge [ (Zge $n1 $n2) ] -> 
       [[<hov 0> "`" (ZEXPR $n1) [1 0] ">= "(ZEXPR $n2) "`" ]]
-  | Zgt [<<(Zgt $n1 $n2)>>] -> 
+  | Zgt [ (Zgt $n1 $n2) ] -> 
       [[<hov 0> "`" (ZEXPR $n1) [1 0] "> "(ZEXPR $n2) "`" ]]
   | Zcompare [<<(Zcompare $n1 $n2)>>] ->
       [[<hov 0> "`" (ZEXPR $n1) [1 0] "?= " (ZEXPR $n2) "`" ]]
-  | Zeq [<<(eq Z $n1 $n2)>>] -> 
+  | Zeq [ (eq Z $n1 $n2) ] -> 
       [[<hov 0> "`" (ZEXPR $n1) [1 0] "= "(ZEXPR $n2)"`"]]
-  | Zneq [<< ~(eq Z $n1 $n2)>>] ->
+  | Zneq [ ~(eq Z $n1 $n2) ] ->
       [[<hov 0> "`" (ZEXPR $n1) [1 0] "<> "(ZEXPR $n2) "`"]]
-  | Zle_Zle [<<(Zle $n1 $n2)/\(Zle $n2 $n3)>>] ->
+  | Zle_Zle [ (Zle $n1 $n2)/\(Zle $n2 $n3) ] ->
       [[<hov 0> "`" (ZEXPR $n1) [1 0] "<= " (ZEXPR $n2)
                                 [1 0] "<= " (ZEXPR $n3) "`"]]
-  | Zle_Zlt [<<(Zle $n1 $n2)/\(Zlt $n2 $n3)>>] ->
+  | Zle_Zlt [ (Zle $n1 $n2)/\(Zlt $n2 $n3) ] ->
       [[<hov 0> "`" (ZEXPR $n1) [1 0] "<= "(ZEXPR $n2)
                                 [1 0] "< " (ZEXPR $n3) "`"]]
-  | Zlt_Zle [<<(Zlt $n1 $n2)/\(Zle $n2 $n3)>>] ->
+  | Zlt_Zle [ (Zlt $n1 $n2)/\(Zle $n2 $n3) ] ->
       [[<hov 0> "`" (ZEXPR $n1) [1 0] "< " (ZEXPR $n2)
                                 [1 0] "<= " (ZEXPR $n3) "`"]]
-  | Zlt_Zlt [<<(Zlt $n1 $n2)/\(Zlt $n2 $n3)>>] ->
+  | Zlt_Zlt [ (Zlt $n1 $n2)/\(Zlt $n2 $n3) ] ->
       [[<hov 0> "`" (ZEXPR $n1) [1 0] "< " (ZEXPR $n2)
                                 [1 0] "< " (ZEXPR $n3) "`"]]
-  | ZZero [<<ZERO>>] -> ["`0`"]
-  | ZPos [<<(POS $r)>>] -> [$r:"positive_printer"]
-  | ZNeg [<<(NEG $r)>>] -> [$r:"negative_printer"]
+  | ZZero [ ZERO ] -> ["`0`"]
+  | ZPos [ (POS $r) ] -> [$r:"positive_printer"]
+  | ZNeg [ (NEG $r) ] -> [$r:"negative_printer"]
   ;
 
   level 7:
-    Zplus [<<(Zplus $n1 $n2)>>]
+    Zplus [ (Zplus $n1 $n2) ]
       -> [ [<hov 0> "`"(ZEXPR $n1):E "+"  [0 0] (ZEXPR $n2):L "`"] ]
-  | Zminus [<<(Zminus $n1 $n2)>>]
+  | Zminus [ (Zminus $n1 $n2) ]
       -> [ [<hov 0> "`"(ZEXPR $n1):E "-" [0 0] (ZEXPR $n2):L "`"] ]
   ;
 
   level 6:
-    Zmult [<<(Zmult $n1 $n2)>>]
+    Zmult [ (Zmult $n1 $n2) ]
       -> [ [<hov 0> "`"(ZEXPR $n1):E "*" [0 0] (ZEXPR $n2):L "`"] ]
   ;
 
   level 8:
-    Zopp [<<(Zopp $n1)>>] -> [ [<hov 0> "`" "-"(ZEXPR $n1):E "`"] ]
-  | Zopp_POS [<<(Zopp (POS $r))>>] -> 
+    Zopp [ (Zopp $n1) ] -> [ [<hov 0> "`" "-"(ZEXPR $n1):E "`"] ]
+  | Zopp_POS [ (Zopp (POS $r)) ] -> 
          [ [<hov 0> "`(" "Zopp" [1 0] $r:"positive_printer_inside"  ")`"] ]
-  | Zopp_ZERO [<<(Zopp ZERO)>>] -> [ [<hov 0> "`(" "Zopp" [1 0] "0" ")`"] ]
-  | Zopp_NEG [<<(Zopp (NEG $r))>>] ->  
+  | Zopp_ZERO [ (Zopp ZERO) ] -> [ [<hov 0> "`(" "Zopp" [1 0] "0" ")`"] ]
+  | Zopp_NEG [ (Zopp (NEG $r)) ] ->  
          [ [<hov 0> "`(" "Zopp" [1 0] "(" $r:"negative_printer_inside" "))`"] ]
   ;
 
   level 4:
-    Zabs [<<(Zabs $n1)>>] -> [  [<hov 0> "`|"(ZEXPR $n1):E "|`"] ]
+    Zabs [ (Zabs $n1) ] -> [  [<hov 0> "`|"(ZEXPR $n1):E "|`"] ]
   ;
 
   level 0:
-    escape_inside [(ZEXPR $r)] -> [ "[" $r:E "]" ]
+    escape_inside [ << (ZEXPR $r) >> ] -> [ "[" $r:E "]" ]
   ;
 
   level 4:
-    Zappl_inside [(ZEXPR (APPLIST $h ($LIST $t)))]
+    Zappl_inside [ << (ZEXPR (APPLIST $h ($LIST $t))) >> ]
       -> [ [<hov 0> "("(ZEXPR $h):E [1 0] (APPLINSIDETAIL ($LIST $t)):E ")"] ]
-  | Zappl_inside_tail [(APPLINSIDETAIL $h ($LIST $t))]
+  | Zappl_inside_tail [ << (APPLINSIDETAIL $h ($LIST $t)) >> ]
       -> [(ZEXPR $h):E [1 0] (APPLINSIDETAIL ($LIST $t)):E] 
-  | Zappl_inside_one [(APPLINSIDETAIL $e)] ->[(ZEXPR $e):E]
-  | pair_inside [(ZEXPR <<(pair $s1 $s2 $z1 $z2)>>)] 
+  | Zappl_inside_one [ << (APPLINSIDETAIL $e) >> ] ->[(ZEXPR $e):E]
+  | pair_inside [ << (ZEXPR <<(pair $s1 $s2 $z1 $z2)>>) >> ] 
       -> [ [<hov 0> "("(ZEXPR $z1):E "," [1 0] (ZEXPR $z2):E ")"] ]
   ;
 
  level 3:
-    var_inside [(ZEXPR ($VAR $i))] -> [$i]
-  | const_inside [(ZEXPR (CONST $c))] -> [(CONST $c)]
-  | mutind_inside [(ZEXPR (MUTIND $i $n))] 
+    var_inside [ << (ZEXPR ($VAR $i)) >> ] -> [$i]
+  | const_inside [ << (ZEXPR (CONST $c)) >> ] -> [(CONST $c)]
+  | mutind_inside [ << (ZEXPR (MUTIND $i $n)) >> ] 
       -> [(MUTIND $i $n)]
-  | mutconstruct_inside [(ZEXPR (MUTCONSTRUCT $c1 $c2 $c3))]
+  | mutconstruct_inside [ << (ZEXPR (MUTCONSTRUCT $c1 $c2 $c3)) >> ]
       -> [ (MUTCONSTRUCT $c1 $c2 $c3) ]
   (* Added by JCF, 9/3/98 *)
-  | implicit_head_inside [(ZEXPR (XTRA "!" $c))] -> [ $c ]
-  | implicit_arg_inside  [(ZEXPR (XTRA "!" $n $c))] -> [ ]
+  | implicit_head_inside [ << (ZEXPR (XTRA "!" $c)) >> ] -> [ $c ]
+  | implicit_arg_inside  [ << (ZEXPR (XTRA "!" $n $c)) >> ] -> [ ]
 
   ;
 
   level 7:
     Zplus_inside
-      [(ZEXPR <<(Zplus $n1 $n2)>>)]
+      [ << (ZEXPR <<(Zplus $n1 $n2)>>) >> ]
       	 -> [ (ZEXPR $n1):E "+" [0 0] (ZEXPR $n2):L ]
   | Zminus_inside
-      [(ZEXPR <<(Zminus $n1 $n2)>>)]
+      [ << (ZEXPR <<(Zminus $n1 $n2)>>) >> ]
       	 -> [ (ZEXPR $n1):E "-" [0 0] (ZEXPR $n2):L ]
   ;
 
   level 6:
     Zmult_inside
-      [(ZEXPR <<(Zmult $n1 $n2)>>)]
+      [ << (ZEXPR <<(Zmult $n1 $n2)>>) >> ]
       	 -> [ (ZEXPR $n1):E "*" [0 0] (ZEXPR $n2):L ]
   ;
 
   level 5:
-    Zopp_inside [(ZEXPR <<(Zopp $n1)>>)] -> [ "(-" (ZEXPR $n1):E ")" ]
+    Zopp_inside [ << (ZEXPR <<(Zopp $n1)>>) >> ] -> [ "(-" (ZEXPR $n1):E ")" ]
   ;  
 
   level 10:
-    Zopp_POS_inside [(ZEXPR <<(Zopp (POS $r))>>)] -> 
+    Zopp_POS_inside [ << (ZEXPR <<(Zopp (POS $r))>>) >> ] -> 
       	 [ [<hov 0> "Zopp" [1 0] $r:"positive_printer_inside" ] ]
-  | Zopp_ZERO_inside [(ZEXPR <<(Zopp ZERO)>>)] -> 
+  | Zopp_ZERO_inside [ << (ZEXPR <<(Zopp ZERO)>>) >> ] -> 
       	 [ [<hov 0> "Zopp" [1 0] "0"] ]
-  | Zopp_NEG_inside [(ZEXPR <<(Zopp (NEG $r))>>)] ->  
+  | Zopp_NEG_inside [ << (ZEXPR <<(Zopp (NEG $r))>>) >> ] ->  
       	 [ [<hov 0> "Zopp" [1 0] $r:"negative_printer_inside" ] ]
   ;
 
   level 4:
-    Zabs_inside [(ZEXPR <<(Zabs $n1)>>)] -> [ "|" (ZEXPR $n1) "|"]
+    Zabs_inside [ << (ZEXPR <<(Zabs $n1)>>) >> ] -> [ "|" (ZEXPR $n1) "|"]
   ;
 
   level 0:
-    ZZero_inside [(ZEXPR <<ZERO>>)] -> ["0"]
-  | ZPos_inside [(ZEXPR <<(POS $p)>>)] -> [$p:"positive_printer_inside"]
-  | ZNeg_inside [(ZEXPR <<(NEG $p)>>)] -> 
+    ZZero_inside [ << (ZEXPR <<ZERO>>) >> ] -> ["0"]
+  | ZPos_inside [ << (ZEXPR <<(POS $p)>>) >>] -> [$p:"positive_printer_inside"]
+  | ZNeg_inside [ << (ZEXPR <<(NEG $p)>>) >> ] -> 
       	       	       	  [$p:"negative_printer_inside"].