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

9 files changed, 367 insertions, 360 deletions

diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index 1dfc5790f..9fa032398 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -192,19 +192,19 @@ END;
 GEXTEND Gram
   GLOBAL: syntax Prim.syntax_entry Prim.grammar_entry;
 
-  grammar_univ:
+  univ:
   [ [ univ = IDENT ->
 	let _ = set_default_action_parser_by_name univ in univ ] ]
   ;
   syntax:
    [ [ "Token"; s = STRING; "." -> <:ast< (TOKEN ($STR $s)) >>
 
-     | "Grammar"; univ = grammar_univ;
+     | "Grammar"; univ = univ;
        tl = LIST1 Prim.grammar_entry SEP "with"; "." ->
          <:ast< (GRAMMAR ($VAR univ) (ASTLIST ($LIST tl))) >>
 
-     | "Syntax"; whatfor=IDENT; el=LIST1 Prim.syntax_entry SEP ";"; "." ->
-         <:ast< (SYNTAX ($VAR whatfor) (ASTLIST ($LIST el))) >>
+     | "Syntax"; univ = univ; el=LIST1 Prim.syntax_entry SEP ";"; "." ->
+         <:ast< (SYNTAX ($VAR univ) (ASTLIST ($LIST el))) >>
      | IDENT "Infix"; as_ = entry_prec; n = numarg; op = Prim.string;
        p = identarg; "." -> <:ast< (INFIX (AST $as_) $n $op $p) >>
      | IDENT "Distfix"; as_ = entry_prec; n = numarg; s = Prim.string;
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 239277828..35d329177 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -46,7 +46,8 @@ GEXTEND Gram
 
   (* meta-syntax entries *)
   astpat:
-    [ [ a = ast -> Node loc "ASTPAT" [a] ] ]
+    [ [ "<<" ; a = ast; ">>" -> Node loc "ASTPAT" [a]
+      | a = default_action_parser -> Node loc "ASTPAT" [a] ] ]
   ; 
   astact:
     [ [ a = action -> Node loc "ASTACT" [a] ] ]
diff --git a/syntax/PPCases.v b/syntax/PPCases.v
index ef328fe77..5f05b9d27 100644
--- a/syntax/PPCases.v
+++ b/syntax/PPCases.v
@@ -3,58 +3,58 @@
 
 Syntax constr
   level 0:
-    ne_command_listcons2 [(NECOMMANDLIST2 $c1 ($LIST $cl))]
+    ne_command_listcons2 [ << (NECOMMANDLIST2 $c1 ($LIST $cl)) >> ]
       -> [ $c1:L [1 0] (NECOMMANDLIST2 ($LIST $cl)) ]
-  | ne_command_listone2 [(NECOMMANDLIST2 $c1)] -> [$c1:L]
+  | ne_command_listone2 [ << (NECOMMANDLIST2 $c1) >> ] -> [$c1:L]
   ;
 
   level 10:
-    as_patt [(PATTAS $var $patt)] -> [$patt:L" as "$var]
+    as_patt [ << (PATTAS $var $patt) >> ] -> [$patt:L" as "$var]
   ;
 
   level 0:
-    ne_pattlist_nil  [(PATTLIST)] -> [ ]
-  | ne_pattlist_cons [(PATTLIST $patt ($LIST $lpatt))]
+    ne_pattlist_nil  [ << (PATTLIST) >> ] -> [ ]
+  | ne_pattlist_cons [ << (PATTLIST $patt ($LIST $lpatt)) >> ]
       -> [$patt:E " " (PATTLIST ($LIST $lpatt))]
   ;
 
   level 8:
-    equation [(EQN $rhs ($LIST $lhs))]
+    equation [ << (EQN $rhs ($LIST $lhs)) >> ]
       -> [ [<hov 0> (PATTLIST ($LIST $lhs)) "=> " [0 1] $rhs:E] ]
   ;
  
   level 0:
-    bar_eqnlist_nil [(BAREQNLIST)] -> [ ]
-  | bar_eqnlist_cons [(BAREQNLIST $eqn ($LIST $leqn))]
+    bar_eqnlist_nil [ << (BAREQNLIST) >> ] -> [ ]
+  | bar_eqnlist_cons [ << (BAREQNLIST $eqn ($LIST $leqn)) >> ]
       -> [ "| " $eqn [1 0] (BAREQNLIST ($LIST $leqn)) ]
-  | bar_eqnlist_one [(BAREQNLIST $eqn)]
+  | bar_eqnlist_one [ << (BAREQNLIST $eqn) >> ]
       -> [ "| " $eqn ]
 
-  | tomatch [(TOMATCH ($LIST $lc))] -> [(NECOMMANDLIST2 ($LIST $lc)):E]
+  | tomatch [ << (TOMATCH ($LIST $lc)) >> ] -> [(NECOMMANDLIST2 ($LIST $lc)):E]
   ;
 
   level 10: 
-    pattconstruct [(PATTCONSTRUCT $C $D ($LIST $T))] ->
+    pattconstruct [ << (PATTCONSTRUCT $C $D ($LIST $T)) >> ] ->
 	 [(APPLIST $C $D ($LIST $T))]
   ;
 
   level 0:
-    pattconstructatomic [(PATTCONSTRUCT $C)] -> [ $C ]
+    pattconstructatomic [ << (PATTCONSTRUCT $C) >> ] -> [ $C ]
   ;
 
   level 8:
 
-    cases_exp_none [(CASES $pred $tomatch)]
+    cases_exp_none [ << (CASES $pred $tomatch) >> ]
       -> [ [<hov 0> (ELIMPRED $pred)
               [<hv 0> "Cases"[1 2] $tomatch:E [1 0] "of"] [1 0] "end"] ]
 
-  | cases_exp_one [(CASES $pred $tomatch $eqn)]
+  | cases_exp_one [ << (CASES $pred $tomatch $eqn) >> ]
       -> [ [<hov 0> (ELIMPRED $pred)
               [<hv 0> [<hv 0> "Cases"[1 2] $tomatch:E [1 0] "of"] [1 2]
                      $eqn [1 0]
                      "end"] ] ]
 
-  | cases_exp_many [(CASES $pred $tomatch $eqn1 $eqn2 ($LIST $eqns))]
+  | cases_exp_many [ << (CASES $pred $tomatch $eqn1 $eqn2 ($LIST $eqns)) >> ]
       -> [ [<hov 0> (ELIMPRED $pred)
               [<v 0> [<hv 0> "Cases"[1 2] $tomatch:E [1 0] "of"] [1 2]
                      $eqn1 [1 0]
@@ -62,29 +62,29 @@ Syntax constr
                      "end"] ] ]
 
   (* "level" indifférent pour ce qui suit *)
-  | let_binder_var [(LETBINDER ($VAR $id))] -> [ $id ]
+  | let_binder_var [ << (LETBINDER ($VAR $id)) >> ] -> [ $id ]
   | let_binder_app 
-	[(LETBINDER (PATTCONSTRUCT $toforget ($VAR $id) ($LIST $vars)))]
+	[<<(LETBINDER (PATTCONSTRUCT $toforget ($VAR $id) ($LIST $vars)))>>]
       -> [ "(" $id (LETBINDERTAIL ($LIST $vars)) ")" ]
  
-  | let_binder_tail_nil  [(LETBINDERTAIL)] -> [ ]
-  | let_binder_tail_cons [(LETBINDERTAIL $var ($LIST $vars))]
+  | let_binder_tail_nil  [ << (LETBINDERTAIL) >> ] -> [ ]
+  | let_binder_tail_cons [ << (LETBINDERTAIL $var ($LIST $vars)) >> ]
       -> [ "," [1 0] $var (LETBINDERTAIL ($LIST $vars)) ]
 
-  | elim_pred      [(ELIMPRED $pred)]          -> [ "<" $pred:E ">" [0 2] ]
-  | elim_pred_xtra [(ELIMPRED "SYNTH")] -> [ ]
+  | elim_pred      [ << (ELIMPRED $pred) >> ]          -> [ "<" $pred:E ">" [0 2] ]
+  | elim_pred_xtra [ << (ELIMPRED "SYNTH") >> ] -> [ ]
   ;
 
   (* On force les parenthèses autour d'un "if" sous-terme (même si le
      parsing est lui plus tolérant) *)
   level 10:
-    boolean_cases [(FORCEIF $pred $tomatch (EQN $c1 $_) (EQN $c2 $_))]
+    boolean_cases [ << (FORCEIF $pred $tomatch (EQN $c1 $_) (EQN $c2 $_)) >> ]
       -> [ [<hov 0> (ELIMPRED $pred)
               [<hv 0> "if " [<hov 0> $tomatch:L ]
                       [1 0] [<hov 0> "then" [1 1] $c1:L ]
                       [1 0] [<hov 0> "else" [1 1] $c2:L ] ] ] ]
 
-  | let_cases [(FORCELET $pred $tomatch (EQN $c $pat))]
+  | let_cases [ << (FORCELET $pred $tomatch (EQN $c $pat)) >> ]
       -> [ [<hov 0> (ELIMPRED $pred)
               [<hv 0> "let " [<hov 0> (LETBINDER $pat) ] " ="
                       [1 1] [<hov 0> $tomatch:L ] ]
diff --git a/syntax/PPConstr.v b/syntax/PPConstr.v
index 766446545..47d92d95d 100755
--- a/syntax/PPConstr.v
+++ b/syntax/PPConstr.v
@@ -5,62 +5,62 @@
 
 Syntax constr
   level 0:
-    ne_command_listcons [(NECOMMANDLIST $c1 ($LIST $cl))]
+    ne_command_listcons [ << (NECOMMANDLIST $c1 ($LIST $cl)) >> ]
        -> [ $c1 [1 0] (NECOMMANDLIST ($LIST $cl)) ]
-  | ne_command_listone [(NECOMMANDLIST $c1)] -> [ $c1 ]
+  | ne_command_listone [ << (NECOMMANDLIST $c1) >> ] -> [ $c1 ]
   ;
 
 (* Things parsed in binder *)
 (* ======================= *)
 
   level 0:
-    idbindercons [(IDBINDER ($VAR $id) ($LIST $L))] ->
+    idbindercons [ << (IDBINDER ($VAR $id) ($LIST $L)) >> ] ->
        [ $id ","[0 0] (IDBINDER ($LIST $L))]
-  | idbinderone  [(IDBINDER ($VAR $id))] -> [$id]
-  | idbindernil  [(IDBINDER)] -> [ ]
+  | idbinderone  [ << (IDBINDER ($VAR $id)) >> ] -> [$id]
+  | idbindernil  [ << (IDBINDER) >> ] -> [ ]
 
-  | binderscons [(BINDERS (BINDER $c ($LIST $id)) ($LIST $b))] ->
+  | binderscons [ << (BINDERS (BINDER $c ($LIST $id)) ($LIST $b)) >> ] ->
        [ [<hv 0> [<hov 0> (IDBINDER ($LIST $id))] ":"
                  [0 1] $c:E] ";"[1 0]
          (BINDERS ($LIST $b))  ]
-  | bindersone  [(BINDERS (BINDER $c ($LIST $id)))] -> 
+  | bindersone  [ << (BINDERS (BINDER $c ($LIST $id))) >> ] -> 
        [ [<hov 0> (IDBINDER ($LIST $id))] ":" $c:E ]
 
-  | letbinder  [(BINDERS (LETBINDER $c $id))] -> 
+  | letbinder  [ << (BINDERS (LETBINDER $c $id)) >> ] -> 
        [ [<hov 0> $id ":=" $c:E ] ]
   ;
 
 
 (* Things parsed in command0 *)
   level 0:
-    prop [(PROP)] -> ["Prop"]
-  | set  [(SET)]  -> ["Set"]
-  | type [(TYPE)] -> ["Type"]
-  | type_sp [(TYPE ($PATH $sp) ($NUM $n))] -> ["Type"]
+    prop [ Prop ] -> ["Prop"]
+  | set  [ Set ]  -> ["Set"]
+  | type [ Type ] -> ["Type"]
+  | type_sp [ << (TYPE ($PATH $sp) ($NUM $n)) >> ] -> ["Type"]
 (* Note: Atomic constants (Nvar, CONST, MUTIND, MUTCONSTRUCT) are printed in
    Printer to know if they must be qualified or not (and previously to
    deal with the duality CCI/FW) *)
 
-  | evar [<< ? >>] -> ["?"]
-  | meta [(META ($NUM $n))] -> [ "?" $n ]
-  | implicit [(IMPLICIT)] -> ["<Implicit>"]
-  | indice [(REL ($NUM $n))] -> ["<Unbound ref: " $n ">"]
-  | instantiation [(INSTANCE $a ($LIST $l))] ->
+  | evar [ ? ] -> ["?"]
+  | meta [ << (META ($NUM $n)) >> ] -> [ "?" $n ]
+  | implicit [ << (IMPLICIT) >> ] -> ["<Implicit>"]
+  | indice [ << (REL ($NUM $n)) >> ] -> ["<Unbound ref: " $n ">"]
+  | instantiation [ << (INSTANCE $a ($LIST $l)) >> ] ->
 	 [ $a "{" (CONTEXT ($LIST $l)) "}"]
-  | instantiation_nil [(CONTEXT)] -> [ ]
-  | instantiation_one [(CONTEXT $a)] -> [ $a ]
-  | instantiation_many [(CONTEXT $a $b ($LIST $l))] ->
+  | instantiation_nil [ << (CONTEXT) >> ] -> [ ]
+  | instantiation_one [ << (CONTEXT $a) >> ] -> [ $a ]
+  | instantiation_many [ << (CONTEXT $a $b ($LIST $l)) >> ] ->
 	 [ (CONTEXT $b ($LIST $l)) ";" $a ]
   ;
 
 (* Things parsed in command1 *)
   level 1:
-    soap [(SOAPP $lc1 ($LIST $cl))]
+    soap [ << (SOAPP $lc1 ($LIST $cl)) >> ]
       -> [ [<hov 0> "(" $lc1 ")@[" (NECOMMANDLIST ($LIST $cl)) "]"] ]
 
   (* For debug *)
-  | abstpatnamed [[$id1]$c] -> [ [<hov 0> "<<" $id1 ">>" [0 1] $c:E ] ]
-  | abstpatanon  [[ <> ]$c] -> [ [<hov 0> "<<_>>" [0 1] $c:E ] ]
+  | abstpatnamed [ << [$id1]$c >> ] -> [ [<hov 0> "<<" $id1 ">>" [0 1] $c:E ] ]
+  | abstpatanon  [ << [ <> ]$c >> ] -> [ [<hov 0> "<<_>>" [0 1] $c:E ] ]
   ;
 
 (* Things parsed in command2 *)
@@ -72,169 +72,172 @@ Syntax constr
 (* Things parsed in command5 *)
 
   level 5:
-    cast [<<($C :: $T)>>] -> [ [<hv 0> $C:L [0 0] "::" $T:E] ]
+    cast [ ($C :: $T) ] -> [ [<hv 0> $C:L [0 0] "::" $T:E] ]
   ;
 (* Things parsed in command6 *)
 
 (* Things parsed in command7 *)
 (* Things parsed in command8 *)
   level 8:
-    lambda [(LAMBDA $Dom [$x]$Body)]
+    lambda [ << (LAMBDA $Dom [$x]$Body) >> ]
      -> [(LAMBOX (BINDERS (BINDER $Dom $x)) $Body)]
-  | lambda_anon [(LAMBDA $Dom [<>]$Body)]
+  | lambda_anon [ << (LAMBDA $Dom [<>]$Body) >> ]
      -> [(LAMBOX (BINDERS (BINDER $Dom _)) $Body)]
-  | lambdalist  [(LAMBDALIST $c [$x]$body)]
+  | lambdalist  [ << (LAMBDALIST $c [$x]$body) >> ]
      -> [(LAMLBOX (BINDERS) $c (IDS $x) $body)]
-  | lambdalist_anon  [(LAMBDALIST $c [<>]$body)]
+  | lambdalist_anon  [ << (LAMBDALIST $c [<>]$body) >> ]
      -> [(LAMLBOX (BINDERS) $c (IDS _) $body)]
 
-  | formated_lambda [(LAMBOX $pbi $t)]
+  | formated_lambda [ << (LAMBOX $pbi $t) >> ]
      -> [ [<hov 0> "[" [<hv 0> $pbi] "]" [0 1] $t:E ] ]
 
-  | lambda_cons [(LAMBOX (BINDERS ($LIST $acc)) (LAMBDA $Dom [$x]$body))]
-      -> [(LAMBOX (BINDERS ($LIST $acc) (BINDER $Dom $x)) $body)]
-  | lambda_cons_anon [(LAMBOX (BINDERS ($LIST $acc)) (LAMBDA $Dom [<>]$body))]
+  | lambda_cons [<<(LAMBOX (BINDERS ($LIST $acc)) (LAMBDA $Dom [$x]$body))>>]
+      -> [(LAMBOX (BINDERS ($LIST $acc) (BINDER $Dom $x)) $body) ]
+  | lambda_cons_anon
+      [ << (LAMBOX (BINDERS ($LIST $acc)) (LAMBDA $Dom [<>]$body)) >> ]
       -> [(LAMBOX (BINDERS ($LIST $acc) (BINDER $Dom _)) $body)]
-  | lambdal_start [(LAMBOX $pbi (LAMBDALIST $Dom $Body))]
+  | lambdal_start [ << (LAMBOX $pbi (LAMBDALIST $Dom $Body)) >> ]
       -> [(LAMLBOX $pbi $Dom (IDS) $Body)]
 
-  | lambdal_end [(LAMLBOX (BINDERS ($LIST $acc)) $c (IDS ($LIST $ids)) $t)]
+  | lambdal_end [<<(LAMLBOX (BINDERS ($LIST $acc)) $c (IDS ($LIST $ids)) $t)>>]
       -> [(LAMBOX (BINDERS ($LIST $acc) (BINDER $c ($LIST $ids))) $t)]
-  | lambdal_cons_anon [(LAMLBOX $pbi $c (IDS ($LIST $ids)) [<>]$body)]
+  | lambdal_cons_anon [ << (LAMLBOX $pbi $c (IDS ($LIST $ids)) [<>]$body) >> ]
       -> [(LAMLBOX $pbi $c (IDS ($LIST $ids) _) $body)]
-  | lambdal_cons [(LAMLBOX $pbi $c (IDS ($LIST $ids)) [$id]$body)]
+  | lambdal_cons [ << (LAMLBOX $pbi $c (IDS ($LIST $ids)) [$id]$body) >> ]
       -> [(LAMLBOX $pbi $c (IDS ($LIST $ids) $id) $body)]
 
-  | pi [<<($x : $A)$B>>] -> [(PRODBOX (BINDERS) <<($x : $A)$B>>)]
-  | prodlist  [(PRODLIST $c $b)]
+  | pi [ ($x : $A)$B ] -> [ (PRODBOX (BINDERS) <<($x : $A)$B>>) ]
+  | prodlist  [ << (PRODLIST $c $b) >> ]
        -> [(PRODBOX (BINDERS) (PRODLIST $c $b))]
 
-  | formated_prod [(PRODBOX $pbi $t)]
+  | formated_prod [ << (PRODBOX $pbi $t) >> ]
      -> [ [<hov 0> "(" [<hov 0> $pbi] ")" [0 1] $t:E ] ]
 
-  | prod_cons [(PRODBOX (BINDERS ($LIST $acc)) <<($x : $Dom)$body>>)]
+  | prod_cons
+      [ << (PRODBOX (BINDERS ($LIST $acc)) <:constr:<($x : $Dom)$body>>) >> ]
       -> [(PRODBOX (BINDERS ($LIST $acc) (BINDER $Dom $x)) $body)]
-  | prodl_start_cons [(PRODBOX $pbi (PRODLIST $Dom $Body))]
+  | prodl_start_cons [ << (PRODBOX $pbi (PRODLIST $Dom $Body)) >> ]
       -> [(PRODLBOX $pbi $Dom (IDS) $Body)]
 
-  | prodl_end [(PRODLBOX (BINDERS ($LIST $acc)) $c (IDS ($LIST $ids)) $t)]
+  | prodl_end [<<(PRODLBOX (BINDERS ($LIST $acc)) $c (IDS ($LIST $ids)) $t)>>]
       -> [(PRODBOX (BINDERS ($LIST $acc) (BINDER $c ($LIST $ids))) $t)]
-  | prodl_cons_anon [(PRODLBOX $pbi $c (IDS ($LIST $ids)) [<>]$body)]
+  | prodl_cons_anon [ << (PRODLBOX $pbi $c (IDS ($LIST $ids)) [<>]$body) >> ]
       -> [(PRODLBOX $pbi $c (IDS ($LIST $ids) _) $body)]
-  | prodl_cons [(PRODLBOX $pbi $c (IDS ($LIST $ids)) [$id]$body)]
+  | prodl_cons [ << (PRODLBOX $pbi $c (IDS ($LIST $ids)) [$id]$body) >> ]
       -> [(PRODLBOX $pbi $c (IDS ($LIST $ids) $id) $body)]
 
 
-  | arrow [<< $A -> $B >>] -> [ [<hv 0> $A:L [0 0] "->" (ARROWBOX $B) ] ]
-  | arrow_stop [(ARROWBOX $c)] -> [ $c:E ]
-  | arrow_again [(ARROWBOX << $A -> $B >>)] -> [ $A:L [0 0] "->" (ARROWBOX $B) ]
+  | arrow [ $A -> $B ] -> [ [<hv 0> $A:L [0 0] "->" (ARROWBOX $B) ] ]
+  | arrow_stop [ << (ARROWBOX $c) >> ] -> [ $c:E ]
+  | arrow_again [ << (ARROWBOX <:constr:< $A -> $B >>) >> ] ->
+	 [ $A:L [0 0] "->" (ARROWBOX $B) ]
 
 (* These are synonymous *)
-  | let [<<[$x = $M]$N>>] -> [ [<hov 0> "[" $x "=" $M:E "]" [0 1] $N:E ] ]
-  | letin [<<[$x := $A]$B>>] -> [ [ <hov 0> "[" $x ":=" $A:E "]" [0 1] $B:E ] ]
+  | let [ [$x = $M]$N ] -> [ [<hov 0> "[" $x "=" $M:E "]" [0 1] $N:E ] ]
+  | letin [ [$x := $A]$B ] -> [ [ <hov 0> "[" $x ":=" $A:E "]" [0 1] $B:E ] ]
   ;
 
 (* Things parsed in command9 *)
 
 (* Things parsed in command10 *)
   level 10:
-    app_cons [(APPLIST $H ($LIST $T))]
+    app_cons [ << (APPLIST $H ($LIST $T)) >> ]
                  -> [ [<hov 0>  $H:E  (APPTAIL ($LIST $T)):E ] ]
 
-  | app_imp  [(APPLISTEXPL $H ($LIST $T))]
+  | app_imp  [ << (APPLISTEXPL $H ($LIST $T)) >> ]
                  -> [ [<hov 0>  "!" $H:E (APPTAIL ($LIST $T)):E ] ]
 
 (*
-  | app_imp  [(APPLISTEXPL $H ($LIST $T))]
+  | app_imp  [ << (APPLISTEXPL $H ($LIST $T)) >> ]
                  -> [ (APPLISTIMPL (ACC $H) ($LIST $T)):E ]
 
-  | app_imp_arg  [(APPLISTIMPL (ACC ($LIST $AC)) $a ($LIST $T))]
+  | app_imp_arg  [ << (APPLISTIMPL (ACC ($LIST $AC)) $a ($LIST $T)) >> ]
         -> [ (APPLISTIMPL (ACC ($LIST $AC) $a) ($LIST $T)):E ]
 
-  | app_imp_imp_arg  [ (APPLISTIMPL $AC (EXPL $_ $_) ($LIST $T)) ]
+  | app_imp_imp_arg  [ << (APPLISTIMPL $AC (EXPL $_ $_) ($LIST $T)) >> ]
        -> [ (APPLISTIMPL $AC ($LIST $T)):E ]
 
-  | app_imp_last [(APPLISTIMPL (ACC ($LIST $A)) $T)]
+  | app_imp_last [ << (APPLISTIMPL (ACC ($LIST $A)) $T) >> ]
          -> [ (APPLIST ($LIST $A) $T):E ]
 *)
 
-  | apptailcons
-       [ (APPTAIL $H ($LIST $T))] -> [ [1 1] $H:L  (APPTAIL ($LIST $T)):E ]
-  | apptailnil [(APPTAIL)] -> [ ]
-  | apptailcons1  [(APPTAIL (EXPL "!" $n $c1) ($LIST $T))]
+  | apptailcons [ << (APPTAIL $H ($LIST $T)) >> ]
+	 -> [ [1 1] $H:L  (APPTAIL ($LIST $T)):E ]
+  | apptailnil [ << (APPTAIL) >> ] -> [ ]
+  | apptailcons1  [ << (APPTAIL (EXPL "!" $n $c1) ($LIST $T)) >> ]
          -> [ [1 1] (EXPL $n $c1):L  (APPTAIL ($LIST $T)):E ]
 
   ;
 
 (* Implicits *)
   level 8:
-    arg_implicit [(EXPL ($NUM $n) $c1)] -> [ $n "!" $c1:L ]
+    arg_implicit [ << (EXPL ($NUM $n) $c1) >> ] -> [ $n "!" $c1:L ]
 (*  | arg_implicit1 [(EXPL "EX" ($NUM $n) $c1)] -> [ $n "!" $c1:L ]
-  | fun_explicit [(EXPL $f)] -> [ $f ]*)
+  | fun_explicit [ << (EXPL $f) >> ] -> [ $f ]*)
   ;
 
 
   level 8:
-    recpr [(XTRA "REC" ($LIST $RECARGS))] -> [ (RECTERM ($LIST $RECARGS)) ]
+    recpr [ << (XTRA "REC" ($LIST $RECARGS)) >> ] -> [ (RECTERM ($LIST $RECARGS)) ]
 
-  | recterm [(RECTERM $P $c ($LIST $BL))] ->
+  | recterm [ << (RECTERM $P $c ($LIST $BL)) >> ] ->
      [ [<hov 0> [<hov 0> "<" $P:E ">"
     		 [0 2] [<hov 0> "Match" [1 1] $c:E  [1 0] "with" ]]
 	         [1 3] [<hov 0> (MATCHBRANCHES ($LIST $BL)):E ] "end"] ]
 
-  | mlcasepr [(XTRA "MLCASE" "NOREC" ($LIST $RECARGS))]
+  | mlcasepr [ << (XTRA "MLCASE" "NOREC" ($LIST $RECARGS)) >> ]
        -> [ (MLCASETERM ($LIST $RECARGS)) ]
 
-  | mlcaseterm [(MLCASETERM $c ($LIST $BL))] ->
+  | mlcaseterm [ << (MLCASETERM $c ($LIST $BL)) >> ] ->
      [ [<hov 0> [<hov 0> "Case" [1 1] $c:E  [1 0] "of" ]
                   [1 3] [<hov 0> (MATCHBRANCHES ($LIST $BL)):E ]"end"] ]
 
-  | mlmatchpr [(XTRA "MLCASE" "REC" ($LIST $RECARGS))]
+  | mlmatchpr [ << (XTRA "MLCASE" "REC" ($LIST $RECARGS)) >> ]
        -> [ (MLMATCHTERM ($LIST $RECARGS)) ]
 
-  | mlmatchterm [(MLMATCHTERM $c ($LIST $BL))] ->
+  | mlmatchterm [ << (MLMATCHTERM $c ($LIST $BL)) >> ] ->
      [ [<hov 0> [<hov 0> "Match" [1 1] $c:E  [1 0] "with" ]
                     [1 3] [<hov 0> (MATCHBRANCHES ($LIST $BL)):E ] "end"] ]
 
 
-  | matchbranchescons [(MATCHBRANCHES $B ($LIST $T))]
+  | matchbranchescons [ << (MATCHBRANCHES $B ($LIST $T)) >> ]
        -> [ [<hov 0> [<hov 0> $B:E ] FNL] (MATCHBRANCHES ($LIST $T)):E ]
-  | matchbranchesnil [(MATCHBRANCHES)] -> [ ]
+  | matchbranchesnil [ << (MATCHBRANCHES) >> ] -> [ ]
 
-  | casepr [(MUTCASE ($LIST $MATCHARGS))] -> [ (CASETERM ($LIST $MATCHARGS)) ]
-  | caseterm [(CASETERM $P $c ($LIST $BL))] ->
+  | casepr [ << (MUTCASE ($LIST $MATCHARGS)) >> ] -> [ (CASETERM ($LIST $MATCHARGS)) ]
+  | caseterm [ << (CASETERM $P $c ($LIST $BL)) >> ] ->
      [ [<hov 0> [<hov 0> "<" $P:E ">"
                   [0 2][<hov 0> "Case" [1 1] $c:E  [1 0] "of" ]]
                   [1 3][<hov 0> (MATCHBRANCHES ($LIST $BL)):E ] "end"] ]
   ;
 
   level 0:
-    fix [(FIX $f $def ($LIST $lfs))] ->
+    fix [ << (FIX $f $def ($LIST $lfs)) >> ] ->
       [ [<hov 0> "Fix " $f
            [0 2] "{" [<v 0> [<hov 0> $def]
                             (FIXDECLS ($LIST $lfs)) ] "}"] ]
 
-  | cofix [(COFIX $f $def ($LIST $lfs))] ->
+  | cofix [ << (COFIX $f $def ($LIST $lfs)) >> ] ->
       [ [<hov 0> "CoFix " $f
            [0 2] "{" [<v 0> [<hov 0> $def]
                             (FIXDECLS ($LIST $lfs)) ] "}"] ]
 
-  | nofixdefs [(FIXDECLS)] -> [ ]
-  | fixdefs [(FIXDECLS $def1 ($LIST $defs))] ->
+  | nofixdefs [ << (FIXDECLS) >> ] -> [ ]
+  | fixdefs [ << (FIXDECLS $def1 ($LIST $defs)) >> ] ->
       [ FNL [<hov 0> "with " $def1] (FIXDECLS ($LIST $defs)) ]
   ;
 
   level 8:
-    onefixnumdecl [(NUMFDECL $f ($NUM $x) $A $t)] ->
+    onefixnumdecl [ << (NUMFDECL $f ($NUM $x) $A $t) >> ] ->
       [ $f "/" $x " :"
         [1 2] $A:E " :="
         [1 2] $t:E ]
-  | onefixdecl [(FDECL $f (BINDERS ($LIST $l)) $A $t)] ->
+  | onefixdecl [ << (FDECL $f (BINDERS ($LIST $l)) $A $t) >> ] ->
       [ $f
         [1 2] "[" [<hv 0> (BINDERS ($LIST $l))] "]"
         [1 2] ": " $A:E " :="
         [1 2] $t:E ]
-  | onecofixdecl [(CFDECL $f $A $t)] ->
+  | onecofixdecl [ << (CFDECL $f $A $t) >> ] ->
       [ $f " : "
         [1 2] $A:E " :="
         [1 2] $t:E ].
diff --git a/syntax/PPTactic.v b/syntax/PPTactic.v
index 769229af2..ad74e4736 100644
--- a/syntax/PPTactic.v
+++ b/syntax/PPTactic.v
@@ -7,309 +7,311 @@
 
 Syntax tactic
   level 3:
-    interpret [(Interpret (TACTIC $t))] -> [ $t:E ]
+    interpret [<<(Interpret (TACTIC $t))>>] -> [ $t:E ]
   ;
 
   (* Put parenthesis when there is more than one tactic *)
   level 3:
-    tacsemilist_many [(TACTICLIST ($LIST $L))]
+    tacsemilist_many [<<(TACTICLIST ($LIST $L))>>]
       -> [ [ <hov 2> (TACTICS ($LIST $L)) ] ]
   ;
 
   level 2:
-    tacsemilist_one [(TACTICLIST $tac)] -> [(TACTICS $tac)]
-  | tacticlist_cons [(TACTICS $t1 ($LIST $l))]
+    tacsemilist_one [<<(TACTICLIST $tac)>>] -> [(TACTICS $tac)]
+  | tacticlist_cons [<<(TACTICS $t1 ($LIST $l))>>]
       -> [ [<hov 0> $t1:E] ";" [1 0] (TACTICS ($LIST $l)) ]
-  | tacticlist_one [(TACTICS $t1)] -> [ [<hov 0> $t1:E] ]
+  | tacticlist_one [<<(TACTICS $t1)>>] -> [ [<hov 0> $t1:E] ]
 
-  | tactic_seq [(TACLIST ($LIST $l))]
+  | tactic_seq [<<(TACLIST ($LIST $l))>>]
              -> [ [<hv 0> "[ " (TACTICSEQBODY ($LIST $l)) " ]" ] ]
 
-  | tacticseqbody_cons [(TACTICSEQBODY $t ($LIST $l))]
+  | tacticseqbody_cons [<<(TACTICSEQBODY $t ($LIST $l))>>]
       -> [ [<hov 0> $t] [1 0] "| " (TACTICSEQBODY ($LIST $l)) ]
-  | tacticseqbody_one  [(TACTICSEQBODY $t)] -> [ [<hov 0> $t] ]
+  | tacticseqbody_one  [<<(TACTICSEQBODY $t)>>] -> [ [<hov 0> $t] ]
   ;
 
   level 1:
-    orelse [(ORELSE $st $tc)] -> [ [<hov 0> $st:L " Orelse" [1 1] $tc:E] ]
+    orelse [ $st Orelse $tc ] -> [ [<hov 0> $st:L " Orelse" [1 1] $tc:E] ]
+
+(*    orelse [ (ORELSE $st $tc)>>] -> [ [<hov 0> $st:L " Orelse" [1 1] $tc:E] ]*)
   ;
 
   level 0:
-    do     [(DO ($NUM $n) $tc)] -> ["Do " $n " " $tc:E]
-  | try    [(TRY $t)]           -> ["Try " $t:E]
-  | info   [(INFO $t)]          -> ["Info " $t:E]
-  | repeat [(REPEAT $tc)]       -> ["Repeat " $tc:E]
-  | first  [(FIRST ($LIST $l))] ->
+    do     [<<(DO ($NUM $n) $tc)>>] -> ["Do " $n " " $tc:E]
+  | try    [<<(TRY $t)>>]           -> ["Try " $t:E]
+  | info   [<<(INFO $t)>>]          -> ["Info " $t:E]
+  | repeat [<<(REPEAT $tc)>>]       -> ["Repeat " $tc:E]
+  | first  [<<(FIRST ($LIST $l))>>] ->
     ["First" [1 0] "[" [1 0] (TACTICSEQBODY ($LIST $l)) [1 0] "]"]
-  | solve  [(TCLSOLVE ($LIST $l))] ->
+  | solve  [<<(TCLSOLVE ($LIST $l))>>] ->
     ["Solve" [1 0] "[" [1 0] (TACTICSEQBODY ($LIST $l)) [1 0] "]"]
 
-  | call [(CALL $macro ($LIST $args))]
+  | call [<<(CALL $macro ($LIST $args))>>]
          -> [ [<hv 3> $macro " " (LISTSPC ($LIST $args)) ] ] 
-  | abstract_anon [(ABSTRACT (TACTIC $t))] 
+  | abstract_anon [<<(ABSTRACT (TACTIC $t))>>] 
          -> ["Abstract " $t:E]
-  | abstract_name [(ABSTRACT ($VAR $id) (TACTIC $t))] 
+  | abstract_name [<<(ABSTRACT ($VAR $id) (TACTIC $t))>>] 
          -> ["Abstract " $t:E " using "  $id]
 
 (* ========================================== *)
 (*       PP rules for simple tactics          *)
 (* ========================================== *)
 
-  | reduce [(Reduce (REDEXP $rexp) $cl)] -> [ (REDEXP $rexp) $cl ]
+  | reduce [<<(Reduce (REDEXP $rexp) $cl)>>] -> [ (REDEXP $rexp) $cl ]
 
-  | split [(Split $b)] -> [ "Split" (WITHBINDING $b) ]
-  | exists [(Exists $b)] -> ["Exists" $b] (* unused! *)
+  | split [<<(Split $b)>>] -> [ "Split" (WITHBINDING $b) ]
+  | exists [<<(Exists $b)>>] -> ["Exists" $b] (* unused! *)
 
-  | auton [(Auto ($NUM $n))] -> ["Auto " $n]
-  | auto_with [(Auto ($LIST $lid))] -> 
+  | auton [<<(Auto ($NUM $n))>>] -> ["Auto " $n]
+  | auto_with [<<(Auto ($LIST $lid))>>] -> 
 	[ "Auto" [1 0] "with " [<hov 0> (LISTSPC ($LIST $lid))] ]
-  | auton_with [(Auto ($NUM $n) ($LIST $lid))] ->
+  | auton_with [<<(Auto ($NUM $n) ($LIST $lid))>>] ->
 	[ "Auto" [1 0] $n [1 0] "with " [<hov 0> (LISTSPC ($LIST $lid))] ]
-  | auto [(Auto)] -> ["Auto"]
+  | auto [<<(Auto)>>] -> ["Auto"]
 
-  | dhyp [(DHyp $id)]  -> ["DHyp " $id]
-  | cdhyp [(CDHyp $id)] -> ["CDHyp " $id]
-  | dconcl [(DConcl)]   -> ["DConcl"] 
-  | superauto [(SuperAuto   $a0 $a1 $a2 $a3)] ->
+  | dhyp [<<(DHyp $id)>>]  -> ["DHyp " $id]
+  | cdhyp [<<(CDHyp $id)>>] -> ["CDHyp " $id]
+  | dconcl [<<(DConcl)>>]   -> ["DConcl"] 
+  | superauto [<<(SuperAuto   $a0 $a1 $a2 $a3)>>] ->
                ["SuperAuto " (AUTOARG $a0) [1 1] 
                              (AUTOARG $a1) [1 1]
                              (AUTOARG $a2) [1 1] 
                              (AUTOARG $a3)]
 
-  | assumption [(Assumption)] -> ["Assumption"]
+  | assumption [<<(Assumption)>>] -> ["Assumption"]
 
-  | intro [(Intro)] -> ["Intro"]
-  | intros [(Intros)] -> ["Intros"]
-  | introsuntil_id [(IntrosUntil $id)] -> ["Intros until " $id]
-  | introsuntil_n [(IntrosUntil ($NUM $n))] -> ["Intros until " $n]
-  | intromove_an [(IntroMove $id)] -> ["Intro after " $id]
-  | intromove_id [(IntroMove $id $id2)] -> ["Intro " $id " after " $id2]
-  | intros_pattern [(INTROPATTERN $p)] -> [$p]
+  | intro [<<(Intro)>>] -> ["Intro"]
+  | intros [<<(Intros)>>] -> ["Intros"]
+  | introsuntil_id [<<(IntrosUntil $id)>>] -> ["Intros until " $id]
+  | introsuntil_n [<<(IntrosUntil ($NUM $n))>>] -> ["Intros until " $n]
+  | intromove_an [<<(IntroMove $id)>>] -> ["Intro after " $id]
+  | intromove_id [<<(IntroMove $id $id2)>>] -> ["Intro " $id " after " $id2]
+  | intros_pattern [<<(INTROPATTERN $p)>>] -> [$p]
 
-  | contradiction [(Contradiction)] -> ["Contradiction"]
+  | contradiction [<<(Contradiction)>>] -> ["Contradiction"]
 
-  | apply [(Apply $c $b)] -> ["Apply " $c (WITHBINDING $b)]
+  | apply [<<(Apply $c $b)>>] -> ["Apply " $c (WITHBINDING $b)]
 
-  | oldelim [(Elim1 $C)] -> ["OldElim " $C]
+  | oldelim [<<(Elim1 $C)>>] -> ["OldElim " $C]
 
-  | elim [(Elim $c $b)] -> ["Elim " $c (WITHBINDING $b)]
-  | elimusing [(Elim $c $b $cu $bu)]
+  | elim [<<(Elim $c $b)>>] -> ["Elim " $c (WITHBINDING $b)]
+  | elimusing [<<(Elim $c $b $cu $bu)>>]
       -> ["Elim " $c (WITHBINDING $b) [1 1]"using " $cu (WITHBINDING $bu)]
 
-  | elimtype [(ElimType $c)] -> ["ElimType " $c]
+  | elimtype [<<(ElimType $c)>>] -> ["ElimType " $c]
 
-  | case_tac [(Case $c $b)] -> ["Case " $c (WITHBINDING $b) ]
+  | case_tac [ << (Case $c $b) >> ] -> ["Case " $c (WITHBINDING $b) ]
 
-  | casetype [(CaseType $c)] -> ["CaseType " $c] 
-  | doubleind [(DoubleInd ($NUM $i) ($NUM $j))]
+  | casetype [<<(CaseType $c)>>] -> ["CaseType " $c] 
+  | doubleind [<<(DoubleInd ($NUM $i) ($NUM $j))>>]
       -> [ "Double Induction " $i " " $j ]
 
-  | specialize [(Specialize $c $b)] -> ["Specialize " $c (WITHBINDING $b)]
-  | specializenum [(Specialize ($NUM $n) $c $b)]
+  | specialize [<<(Specialize $c $b)>>] -> ["Specialize " $c (WITHBINDING $b)]
+  | specializenum [<<(Specialize ($NUM $n) $c $b)>>]
       -> ["Specialize " $n " " $c (WITHBINDING $b) ]
 
-  | generalize [(Generalize ($LIST $lc))]
+  | generalize [<<(Generalize ($LIST $lc))>>]
       -> [ [<hov 3> "Generalize " (LISTSPC ($LIST $lc))] ]
 
-  | lapply [(CutAndApply $c)] -> ["LApply " $c]
+  | lapply [<<(CutAndApply $c)>>] -> ["LApply " $c]
 
-  | clear [(Clear (CLAUSE ($LIST $l)))] ->
+  | clear [<<(Clear (CLAUSE ($LIST $l)))>>] ->
           [ [<hov 3> "Clear " (LISTSPC ($LIST $l))] ]
 
-  | move [(MoveDep $id1 $id2)] ->
+  | move [<<(MoveDep $id1 $id2)>>] ->
           [ "Move " $id1 " after " $id2 ]
 
-  | constructor [(Constructor)] -> ["Constructor" ]
-  | constructor_num [(Constructor ($NUM $n) $b)]
+  | constructor [<<(Constructor)>>] -> ["Constructor" ]
+  | constructor_num [<<(Constructor ($NUM $n) $b)>>]
       -> ["Constructor " $n (WITHBINDING $b) ]
 
-  | trivial [(Trivial)] -> ["Trivial"]
+  | trivial [<<(Trivial)>>] -> ["Trivial"]
 
-  | failingtrivial [(FailingTrivial)] -> ["Trivial"]
+  | failingtrivial [<<(FailingTrivial)>>] -> ["Trivial"]
 
-  | inductionid [(Induction $id)] -> ["Induction " $id]
-  | inductionnum [(Induction ($NUM $n))] -> ["Induction " $n]
+  | inductionid [<<(Induction $id)>>] -> ["Induction " $id]
+  | inductionnum [<<(Induction ($NUM $n))>>] -> ["Induction " $n]
 
-  | destructid [(Destruct $id)] -> ["Destruct " $id]
-  | destructnum [(Destruct ($NUM $n))] -> ["Destruct " $n]
+  | destructid [<<(Destruct $id)>>] -> ["Destruct " $id]
+  | destructnum [<<(Destruct ($NUM $n))>>] -> ["Destruct " $n]
 
-  | decomposeand [(DecomposeAnd $c)] -> [ "Decompose Record " $c ]
-  | decomposeor [(DecomposeOr $c)] -> [ "Decompose Sum " $c ]
-  | decomposethese [(DecomposeThese (CLAUSE ($LIST $l)) $c )] -> 
+  | decomposeand [<<(DecomposeAnd $c)>>] -> [ "Decompose Record " $c ]
+  | decomposeor [<<(DecomposeOr $c)>>] -> [ "Decompose Sum " $c ]
+  | decomposethese [<<(DecomposeThese (CLAUSE ($LIST $l)) $c )>>] -> 
               ["Decompose" [1 1] [<hov 0> "[" (LISTSPC ($LIST $l)) "]" ] 
 	                         [1 1] $c]
-  | mutualcofixtactic [(Cofix $id $cfe ($LIST $fd))] 
+  | mutualcofixtactic [<<(Cofix $id $cfe ($LIST $fd))>>] 
       -> ["Cofix "  $id  [1 1]"with " [<hov 0> $cfe (FIXLIST ($LIST $fd))] ]
-  | pp_simple_cofix_tactic [(Cofix)] -> ["Cofix"]
-  | pp_cofix_tactic [(Cofix $id)] -> ["Cofix " $id]
-  | cofixexp [(COFIXEXP $id $c)] -> [ $id ":" $c ]
+  | pp_simple_cofix_tactic [<<(Cofix)>>] -> ["Cofix"]
+  | pp_cofix_tactic [<<(Cofix $id)>>] -> ["Cofix " $id]
+  | cofixexp [<<(COFIXEXP $id $c)>>] -> [ $id ":" $c ]
 
-  | mutualfixtactic [(Fix $id $n $cfe ($LIST $fd))] 
+  | mutualfixtactic [<<(Fix $id $n $cfe ($LIST $fd))>>] 
       -> ["Fix " $id " " $n [1 1]"with " [<hov 0> $cfe (FIXLIST ($LIST $fd))] ]
-  | pp_simple_fix_tactic [(Fix ($NUM $n))] -> ["Fix " $n]
-  | pp_fix_tactic [(Fix $id ($NUM $n))] -> ["Fix " $id " " $n]
-  | fixexp [(FIXEXP $id ($NUM $n) $c)] -> [ $id " " $n ":" $c ]
+  | pp_simple_fix_tactic [<<(Fix ($NUM $n))>>] -> ["Fix " $n]
+  | pp_fix_tactic [<<(Fix $id ($NUM $n))>>] -> ["Fix " $id " " $n]
+  | fixexp [<<(FIXEXP $id ($NUM $n) $c)>>] -> [ $id " " $n ":" $c ]
 
-  | fixdeclcons [(FIXLIST $cfe ($LIST $fd))]
+  | fixdeclcons [<<(FIXLIST $cfe ($LIST $fd))>>]
       -> [ [1 0] $cfe (FIXLIST ($LIST $fd))]
-  | fixdeclnil  [(FIXLIST)] -> [ ]
+  | fixdeclnil  [<<(FIXLIST)>>] -> [ ]
 
-  | exact [(Exact $C)] -> ["Exact " $C]
+  | exact [<<(Exact $C)>>] -> ["Exact " $C]
 
-  | absurd [(Absurd $C)] -> ["Absurd " $C]
+  | absurd [<<(Absurd $C)>>] -> ["Absurd " $C]
 
-  | cut [(Cut $C)] -> ["Cut " $C]
-  | lettac [(LetTac $id $c (LETPATTERNS ($LIST $pl)))] -> 
+  | cut [<<(Cut $C)>>] -> ["Cut " $C]
+  | lettac [<<(LetTac $id $c (LETPATTERNS ($LIST $pl)))>>] -> 
 	["LetTac" [1 1] $id ":=" $c [1 1] "in" [1 1] (LETPATTERNS ($LIST $pl))]
 
-  | left [(Left $b)] -> ["Left" (WITHBINDING $b)]
-  | right [(Right $b)] -> [ "Right" (WITHBINDING $b)]
+  | left [<<(Left $b)>>] -> ["Left" (WITHBINDING $b)]
+  | right [<<(Right $b)>>] -> [ "Right" (WITHBINDING $b)]
 
-  | discriminate [(Discriminate)] -> ["Simple Discriminate"]
+  | discriminate [<<(Discriminate)>>] -> ["Simple Discriminate"]
 
-  | reflexivity [(Reflexivity)] -> ["Reflexivity"]
-  | symmetry [(Symmetry)] -> ["Symmetry"]
-  | transitivity [(Transitivity $C)] -> ["Transitivity " $C]
+  | reflexivity [<<(Reflexivity)>>] -> ["Reflexivity"]
+  | symmetry [<<(Symmetry)>>] -> ["Symmetry"]
+  | transitivity [<<(Transitivity $C)>>] -> ["Transitivity " $C]
 
-  | idtac [(Idtac)] -> ["Idtac"]
+  | idtac [<<(Idtac)>>] -> ["Idtac"]
 
 
 (* ============================================== *)
 (*      PP rules for tactic arguments             *)
 (* ============================================== *)
 
-  | idargnil [(IDARGLIST)] -> [ ]
+  | idargnil [<<(IDARGLIST)>>] -> [ ]
   | idargcons
-      [(IDARGLIST $id ($LIST $L))] -> [ $id " "  (IDARGLIST ($LIST $L)) ]
+      [<<(IDARGLIST $id ($LIST $L))>>] -> [ $id " "  (IDARGLIST ($LIST $L)) ]
 
   | nenumlistcons
-      [(NENUMLIST ($NUM $n) ($LIST $l))] -> [ $n " " (NENUMLIST ($LIST $l)) ]
-  | nenumlistone [(NENUMLIST ($NUM $n))] -> [ $n ]
+      [<<(NENUMLIST ($NUM $n) ($LIST $l))>>] -> [ $n " " (NENUMLIST ($LIST $l)) ]
+  | nenumlistone [<<(NENUMLIST ($NUM $n))>>] -> [ $n ]
 
-  | numlistcons [(NUMLIST ($LIST $l))] -> [ (NENUMLIST ($LIST $l)) ]
-  | numlistnil [(NUMLIST)] -> [ ]
+  | numlistcons [<<(NUMLIST ($LIST $l))>>] -> [ (NENUMLIST ($LIST $l)) ]
+  | numlistnil [<<(NUMLIST)>>] -> [ ]
 
   (* Bindings: print "with" before the bindings. *)
-  | with_binding [(WITHBINDING (BINDINGS ($LIST $b)))]
+  | with_binding [<<(WITHBINDING (BINDINGS ($LIST $b)))>>]
        -> [ [1 1] "with " [<hov 0> (BINDBOX ($LIST $b)) ] ]
-  | without_binding [(WITHBINDING (BINDINGS))] -> [ ]
+  | without_binding [<<(WITHBINDING (BINDINGS))>>] -> [ ]
 
   (* Bindings: nor break nor "with" before. *)
-  | bindings [(BINDINGS ($LIST $l))] -> [ " " [<hov 0> (BINDBOX ($LIST $l)) ] ]
-  | bindingsnone [(BINDINGS)] -> [ ]
+  | bindings [<<(BINDINGS ($LIST $l))>>] -> [ " " [<hov 0> (BINDBOX ($LIST $l)) ] ]
+  | bindingsnone [<<(BINDINGS)>>] -> [ ]
 
   (* Prints a non-empty list of bindings, assuming the box and the first space
      is already printed. *)
-  | bindinglistcons [(BINDBOX $b ($LIST $bl))]
+  | bindinglistcons [<<(BINDBOX $b ($LIST $bl))>>]
       -> [ $b [1 0] (BINDBOX ($LIST $bl)) ]
-  | bindinglistone [(BINDBOX $b)] -> [ $b ]
+  | bindinglistone [<<(BINDBOX $b)>>] -> [ $b ]
 
   (* One binding *)
-  | bindingid [(BINDING ($VAR $id) $c)] -> [ [<hov 2> $id ":=" $c ] ]
-  | bindingnum [(BINDING ($NUM $n) $c)] -> [ [<hov 2> $n ":=" $c ] ]
-  | bindingcom [(BINDING $c)] -> [ $c ]
-
-  | reduce_red [(REDEXP (Red))] -> ["Red"]
-  | reduce_hnf [(REDEXP (Hnf))] -> ["Hnf"]
-  | reduce_simpl [(REDEXP (Simpl))] -> ["Simpl"]
-  | reduce_cbv [(REDEXP (Cbv ($LIST $lf)))] -> ["Cbv" (FLAGS ($LIST $lf))]
-  | reduce_compute [(REDEXP (Cbv (Beta) (Delta) (Iota)))] -> [ "Compute" ]
-  | reduce_lazy [(REDEXP (Lazy ($LIST $lf)))] -> ["Lazy" (FLAGS ($LIST $lf))]
-  | reduce_unfold [(REDEXP (Unfold ($LIST $unf)))] ->
+  | bindingid [<<(BINDING ($VAR $id) $c)>>] -> [ [<hov 2> $id ":=" $c ] ]
+  | bindingnum [<<(BINDING ($NUM $n) $c)>>] -> [ [<hov 2> $n ":=" $c ] ]
+  | bindingcom [<<(BINDING $c)>>] -> [ $c ]
+
+  | reduce_red [<<(REDEXP (Red))>>] -> ["Red"]
+  | reduce_hnf [<<(REDEXP (Hnf))>>] -> ["Hnf"]
+  | reduce_simpl [<<(REDEXP (Simpl))>>] -> ["Simpl"]
+  | reduce_cbv [<<(REDEXP (Cbv ($LIST $lf)))>>] -> ["Cbv" (FLAGS ($LIST $lf))]
+  | reduce_compute [<<(REDEXP (Cbv (Beta) (Delta) (Iota)))>>] -> [ "Compute" ]
+  | reduce_lazy [<<(REDEXP (Lazy ($LIST $lf)))>>] -> ["Lazy" (FLAGS ($LIST $lf))]
+  | reduce_unfold [<<(REDEXP (Unfold ($LIST $unf)))>>] ->
        [ [<hv 3> "Unfold " (UNFOLDLIST ($LIST $unf))] ]
-  | reduce_fold [(REDEXP (Fold ($LIST $cl)))] ->
+  | reduce_fold [<<(REDEXP (Fold ($LIST $cl)))>>] ->
        [ [<hov 3> "Fold " (LISTSPC ($LIST $cl))] ]
-  | reduce_change [(REDEXP (Change $c))] -> ["Change " $c]
-  | reduce_pattern [(REDEXP (Pattern ($LIST $pl)))] ->
+  | reduce_change [<<(REDEXP (Change $c))>>] -> ["Change " $c]
+  | reduce_pattern [<<(REDEXP (Pattern ($LIST $pl)))>>] ->
        [ [<hv 3> "Pattern " (NEPATTERNLIST ($LIST $pl)) ] ]
 
-  | flags_beta [(FLAGS (Beta) ($LIST $F))] ->
+  | flags_beta [<<(FLAGS (Beta) ($LIST $F))>>] ->
         [ [1 0] "Beta" (FLAGS ($LIST $F))]
-  | flags_delta [(FLAGS (Delta) ($LIST $F))] ->
+  | flags_delta [<<(FLAGS (Delta) ($LIST $F))>>] ->
         [ [1 0] "Delta" (FLAGS ($LIST $F))]
-  | flags_iota [(FLAGS (Iota) ($LIST $F))] ->
+  | flags_iota [<<(FLAGS (Iota) ($LIST $F))>>] ->
         [ [1 0] "Iota" (FLAGS ($LIST $F))]
-  | delta_unf [(FLAGS (Unf ($LIST $idl)))]
+  | delta_unf [<<(FLAGS (Unf ($LIST $idl)))>>]
          -> [ [1 0] "[" [<hov 0> (LISTSPC ($LIST $idl)) ] "]" ]
-  | delta_unfbut [(FLAGS (UnfBut ($LIST $idl)))]
+  | delta_unfbut [<<(FLAGS (UnfBut ($LIST $idl)))>>]
          -> [ [1 0] "-[" [<hov 0> (LISTSPC ($LIST $idl)) ] "]" ]
-  | flags_nil [(FLAGS)] -> [ ]
+  | flags_nil [<<(FLAGS)>>] -> [ ]
 
 
   | unfoldcons
-        [(UNFOLDLIST $H ($LIST $T))] -> [ $H " " (UNFOLDLIST ($LIST $T)) ]
-  | unfoldone [(UNFOLDLIST $H)] -> [ $H ]
+        [<<(UNFOLDLIST $H ($LIST $T))>>] -> [ $H " " (UNFOLDLIST ($LIST $T)) ]
+  | unfoldone [<<(UNFOLDLIST $H)>>] -> [ $H ]
 
-  | unfoldarg [(UNFOLD $id ($LIST $OCCL))]
+  | unfoldarg [<<(UNFOLD $id ($LIST $OCCL))>>]
          -> [ (UNFOLDOCCLIST ($LIST $OCCL)) (COMMAND $id) ]
 
-  | unfold_occ_nil  [(UNFOLDOCCLIST)] -> [ ]
-  | unfold_occ_cons [(UNFOLDOCCLIST ($NUM $n) ($LIST $T))]
+  | unfold_occ_nil  [<<(UNFOLDOCCLIST)>>] -> [ ]
+  | unfold_occ_cons [<<(UNFOLDOCCLIST ($NUM $n) ($LIST $T))>>]
          -> [ $n " " (UNFOLDOCCLIST ($LIST $T)) ]
 
 
-  | autoarg_depth     [(AUTOARG $n)] -> [ $n]
-  | autoarg_adding1   [(AUTOARG (CLAUSE ($LIST $l)))] -> 
+  | autoarg_depth     [<<(AUTOARG $n)>>] -> [ $n]
+  | autoarg_adding1   [<<(AUTOARG (CLAUSE ($LIST $l)))>>] -> 
                       ["Adding" [1 1] "[" (LISTSPC ($LIST $l)) "]"]
 
-  | autoarg_adding2     [(AUTOARG (CLAUSE))] -> [""]
-  | autoarg_destructing [(AUTOARG "Destructing")] -> 
+  | autoarg_adding2     [<<(AUTOARG (CLAUSE))>>] -> [""]
+  | autoarg_destructing [<<(AUTOARG "Destructing")>>] -> 
                         ["Destructing"]
-  | autoarg_usingTDB    [(AUTOARG "UsingTDB")]    -> ["Using TDB"]
-  | autoarg_noarg       [(AUTOARG "NoAutoArg")]   -> [""]
+  | autoarg_usingTDB    [<<(AUTOARG "UsingTDB")>>]    -> ["Using TDB"]
+  | autoarg_noarg       [<<(AUTOARG "NoAutoArg")>>]   -> [""]
   
-  | intropatlist [(LISTPATTERN ($LIST $tl))] ->
+  | intropatlist [<<(LISTPATTERN ($LIST $tl))>>] ->
                  [ (LISTSPC ($LIST $tl)) ]
-  | intropatdisj [(DISJPATTERN ($LIST $dp))] ->
+  | intropatdisj [<<(DISJPATTERN ($LIST $dp))>>] ->
                  [ "[" [<hv 0> (LISTBAR ($LIST $dp))] "]" ]
-  | intropatconj [(CONJPATTERN ($LIST $cp))] ->
+  | intropatconj [<<(CONJPATTERN ($LIST $cp))>>] ->
                  [ "(" [<hov 0> (LISTCOMA ($LIST $cp))] ")" ]
-  | intropatid [(IDENTIFIER ($VAR $id))] -> [ $id ]
+  | intropatid [<<(IDENTIFIER ($VAR $id))>>] -> [ $id ]
 
 
-  | patterncons [(NEPATTERNLIST $H ($LIST $T))]
+  | patterncons [<<(NEPATTERNLIST $H ($LIST $T))>>]
          -> [ [<hov 1> $H ] [1 0] (NEPATTERNLIST ($LIST $T)) ]
-  | patternone [(NEPATTERNLIST $H)] -> [ [<hov 1> $H ] ]
+  | patternone [<<(NEPATTERNLIST $H)>>] -> [ [<hov 1> $H ] ]
 
-  | patternargoccs [(PATTERN $c ($LIST $OCCL))]
+  | patternargoccs [<<(PATTERN $c ($LIST $OCCL))>>]
          -> [ [<hov 1> (NENUMLIST ($LIST $OCCL)) ] [1 1] $c ]
-  | patternargnil [(PATTERN $c)] -> [ $c ]
+  | patternargnil [<<(PATTERN $c)>>] -> [ $c ]
 
 
-  | letpatterncons [(LETPATTERNS $H ($LIST $T))]
+  | letpatterncons [<<(LETPATTERNS $H ($LIST $T))>>]
          -> [ [<hov 1> $H ] [1 0] (LETPATTERNS ($LIST $T)) ]
-  | letpatternone [(LETPATTERNS $H)] -> [ [<hov 1> $H ] ]
+  | letpatternone [<<(LETPATTERNS $H)>>] -> [ [<hov 1> $H ] ]
 
-  | hyppatternargoccs [(HYPPATTERN $s ($LIST $OCCL))]
+  | hyppatternargoccs [<<(HYPPATTERN $s ($LIST $OCCL))>>]
          -> [ [<hov 1> (NENUMLIST ($LIST $OCCL)) ] [1 1] $s ]
-  | hyppatternargnil [(HYPPATTERN $s)] -> [ $s ]
+  | hyppatternargnil [<<(HYPPATTERN $s)>>] -> [ $s ]
 
-  | cclpatternargoccs [(CCLPATTERN ($LIST $OCCL))]
+  | cclpatternargoccs [<<(CCLPATTERN ($LIST $OCCL))>>]
          -> [ [<hov 1> (NENUMLIST ($LIST $OCCL)) ] [1 1] "Goal" ]
-  | cclpatternargnil [(CCLPATTERN)] -> [ "Goal" ]
+  | cclpatternargnil [<<(CCLPATTERN)>>] -> [ "Goal" ]
 
 
-  | clause [(CLAUSE ($LIST $l))]
+  | clause [<<(CLAUSE ($LIST $l))>>]
          -> [ [1 1][<hov 2> "in " (LISTSPC ($LIST $l)) ] ]
-  | clause_none [(CLAUSE)] -> [ ]
+  | clause_none [<<(CLAUSE)>>] -> [ ]
 
 
   (* Lists with separators *)
-  | listspc_cons [(LISTSPC $x ($LIST $l))] ->
+  | listspc_cons [<<(LISTSPC $x ($LIST $l))>>] ->
                  [ $x [1 0] (LISTSPC ($LIST $l)) ]
-  | listspc_one  [(LISTSPC $x)] -> [ $x ]
-  | listspc_nil  [(LISTSPC )] -> [ ]
+  | listspc_one  [<<(LISTSPC $x)>>] -> [ $x ]
+  | listspc_nil  [<<(LISTSPC )>>] -> [ ]
 
-  | listbar_cons [(LISTBAR $x ($LIST $l))] ->
+  | listbar_cons [<<(LISTBAR $x ($LIST $l))>>] ->
                  [ $x [1 0]"| " (LISTBAR ($LIST $l)) ]
-  | listbar_one  [(LISTBAR $x)] -> [ $x ]
-  | listbar_nil  [(LISTBAR )] -> [ ]
+  | listbar_one  [<<(LISTBAR $x)>>] -> [ $x ]
+  | listbar_nil  [<<(LISTBAR )>>] -> [ ]
 
-  | listcoma_cons [(LISTCOMA $x ($LIST $l))] ->
+  | listcoma_cons [<<(LISTCOMA $x ($LIST $l))>>] ->
                   [ $x ","[1 0] (LISTCOMA ($LIST $l)) ]
-  | listcoma_one  [(LISTCOMA $x)] -> [ $x ]
-  | listcoma_nil  [(LISTCOMA )] -> [ ]
+  | listcoma_one  [<<(LISTCOMA $x)>>] -> [ $x ]
+  | listcoma_nil  [<<(LISTCOMA )>>] -> [ ]
   ;
 
   level 8:
-  tactic_to_constr [(COMMAND $c)] -> [ $c:"constr":9 ].
+  tactic_to_constr [<<(COMMAND $c)>>] -> [ $c:"constr":9 ].
diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v
index 57b76e017..06aa13102 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 6760bcafa..5064ddcec 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 a3a69c310..33f5fad72 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 350bcaa18..df7551e6a 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"].