Plus de piquants dans les actions des grammaires; nom de la grammaire pris comme parseur par defaut; le type List devient AstList

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

14 files changed, 132 insertions, 80 deletions

diff --git a/CHANGES b/CHANGES
index 9e29a7e502..f8cb0a4109 100644
--- a/CHANGES
+++ b/CHANGES
@@ -16,3 +16,9 @@
 - Ajout de la syntaxe "[" phrase_1 ... phrase_n"]." pour grouper des
 phrases (utile pour Time et pour des grammaires abrégeant plusieurs
 commandes)
+
+- Le parseur par défaut des actions des règles de grammaires est
+maintenant celui associé au nom de la grammaire (vernac, tactic ou
+constr). Donc plus de piquants <:vernac:<...>> etc. Pour retourner de
+l'ast, il faut typer explicitement la grammaire avec Ast ou List
+(renommé d'ailleurs AstList).
diff --git a/parsing/ast.ml b/parsing/ast.ml
index e7c6cb23c7..d154b79701 100755
--- a/parsing/ast.ml
+++ b/parsing/ast.ml
@@ -544,16 +544,12 @@ let rec act_of_ast vars etyp ast =
            | ETastl ->
                let acl = List.map (caselist vars etyp) cl in
                Acaselist (pa,acl))
-    | Node(_,"ASTLIST",al) ->
-        (match (etyp,al) with
-           | (ETast,[a]) -> Aast (val_of_ast vars a)
-           | (ETastl,_) -> Aastlist (vall_of_astl vars al)
-           | (ETast,_) -> user_err_loc
-                 (loc ast,"Ast.act_of_ast",
-                  [< 'sTR
-                       "entry type is Ast, but the right hand side is a list"
-                  >]))
-    | _ -> invalid_arg_loc (loc ast,"Ast.act_of_ast: ill-formed")
+    | Node(_,"ASTLIST",al) when etyp = ETastl ->
+	Aastlist (vall_of_astl vars al)
+    | a when etyp = ETast ->
+	  Aast (val_of_ast vars a)
+    | _ ->
+	invalid_arg_loc (loc ast,"Ast.act_of_ast: ill-typed")
 
 and case vars etyp ast =
   match ast with
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 002925e167..9065d565c7 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -418,12 +418,17 @@ let dbize k sigma env allow_soapp lvar =
 	    else 
 	      (RHole None)::(aux (n+1) l' args)
 	  else 
-	    error "Bad explicitation number"
+	    if i<>n then
+	      error ("Bad explicitation number: found "^
+		   (string_of_int j)^" but was expecting a regular argument")
+	    else
+	      error ("Bad explicitation number: found "^
+		   (string_of_int j)^" but was expecting "^(string_of_int i))
       | (i::l',a::args') -> 
 	  if i=n then 
 	    (RHole None)::(aux (n+1) l' args)
 	  else 
-	    (dbrec env a)::(aux (n+1) l' args')
+	    (dbrec env a)::(aux (n+1) l args')
       | ([],args) -> List.map (dbrec env) args
       | (_,[]) -> []
     in 
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index ad1fbd1b55..b8534a8730 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -172,10 +172,15 @@ END;
 GEXTEND Gram
   GLOBAL: syntax Prim.syntax_entry Prim.grammar_entry;
 
+  grammar_univ:
+  [ [ univ = IDENT ->
+	let _ = set_default_action_parser_by_name univ in univ ] ]
+  ;
   syntax:
    [ [ "Token"; s = STRING; "." -> <:ast< (TOKEN ($STR $s)) >>
 
-     | "Grammar"; univ=IDENT; tl=LIST1 Prim.grammar_entry SEP "with"; "." ->
+     | "Grammar"; univ = grammar_univ;
+       tl = LIST1 Prim.grammar_entry SEP "with"; "." ->
          <:ast< (GRAMMAR ($VAR univ) (ASTLIST ($LIST tl))) >>
 
      | "Syntax"; whatfor=IDENT; el=LIST1 Prim.syntax_entry SEP ";"; "." ->
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 7be07ea0d1..239277828f 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -60,14 +60,18 @@ GEXTEND Gram
       | IDENT "case"; a = action; et = entry_type; "of";
         cl = LIST1 case SEP "|"; IDENT "esac" ->
           Node(loc,"$CASE",a::et::cl)
-      | "["; al = astlist; "]" -> al ] ]
+      | "["; al = default_action_parser; "]" -> al ] ]
   ;
   case:
     [[ p = astlist; "->"; a = action -> Node(loc,"CASE",[p;a]) ]]
   ;
   entry_type:
-    [[ ":"; IDENT "List" -> Id(loc,"LIST")
-     | ":"; IDENT "Ast" -> Id(loc,"AST")
+    [[ ":"; IDENT "AstList" -> 
+	 let _ = set_default_action_parser astlist in Id(loc,"LIST")
+     | ":"; IDENT "List" -> (* For compatibility *)
+	 let _ = set_default_action_parser astlist in Id(loc,"LIST")
+     | ":"; IDENT "Ast" ->
+	 let _ = set_default_action_parser ast in Id(loc,"AST")
      | -> Id(loc,"AST") ]]
   ;
 END
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 951a576c8f..a80952480e 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -390,20 +390,49 @@ END
 (* Quotations *)
 
 open Prim
+open Constr
+open Tactic
+open Vernac
 
 let define_quotation default s e =
   (if default then
     GEXTEND Gram
       ast: [ [ "<<"; c = e; ">>" -> c ] ];
+     (* Uncomment this to keep compatibility with old grammar syntax
+     constr: [ [ "<<"; c = e; ">>" -> c ] ];
+     vernac: [ [ "<<"; c = e; ">>" -> c ] ];
+     tactic: [ [ "<<"; c = e; ">>" -> c ] ];
+     *)
    END);
   (GEXTEND Gram
-     GLOBAL: ast;
+     GLOBAL: ast constr vernac tactic;
      ast:
-       [ [ _ = langle_colon; IDENT $s$; _ = colon_langle; c = e; ">>" -> c ] ];
-     langle_colon:
-       [ [ "<"; ":" -> ()
-	 | "<:" -> () ] ];  (* Maximal token rule *)
-     colon_langle:
-       [ [ ":"; "<" -> ()
-	 | ":<" -> () ] ]; (* Maximal token rule *)
+       [ [ "<:"; IDENT $s$; ":<"; c = e; ">>" -> c ] ];
+     (* Uncomment this to keep compatibility with old grammar syntax
+     constr:
+       [ [ "<:"; IDENT $s$; ":<"; c = e; ">>" -> c ] ];
+     vernac:
+       [ [ "<:"; IDENT $s$; ":<"; c = e; ">>" -> c ] ];
+     tactic:
+       [ [ "<:"; IDENT $s$; ":<"; c = e; ">>" -> c ] ];
+     *)
    END)
+
+let _ = define_quotation false "ast" ast in ()
+
+let default_action_parser_ref = ref ast
+
+let get_default_action_parser () = !default_action_parser_ref
+
+let set_default_action_parser f = (default_action_parser_ref := f)
+
+let set_default_action_parser_by_name = function
+  | "constr" -> set_default_action_parser Constr.constr
+  | "tactic" -> set_default_action_parser Tactic.tactic
+  | "vernac" -> set_default_action_parser Vernac.vernac
+  | _ -> set_default_action_parser ast
+
+let default_action_parser =
+  Gram.Entry.of_parser "default_action_parser" 
+    (fun strm -> Gram.Entry.parse_token (get_default_action_parser ()) strm)
+
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index a60bfec5e8..2d486e5617 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -52,6 +52,12 @@ val force_entry_type : string * gram_universe -> string ->
 
 val define_quotation : bool -> string -> (Coqast.t Gram.Entry.e) -> unit
 
+(* The default parser for actions in grammar rules *)
+
+val default_action_parser : Coqast.t Gram.Entry.e
+val set_default_action_parser : Coqast.t Gram.Entry.e -> unit
+val set_default_action_parser_by_name : string -> unit
+
 (* The main entry: reads an optional vernac command *)
 
 val main_entry : Coqast.t option Gram.Entry.e
diff --git a/tactics/EAuto.v b/tactics/EAuto.v
index c03334aebd..f56d9aadc1 100644
--- a/tactics/EAuto.v
+++ b/tactics/EAuto.v
@@ -13,7 +13,7 @@
 (*                                 Prolog.v                                 *)
 (****************************************************************************)
 
-Grammar tactic simple_tactic :=
+Grammar tactic simple_tactic: Ast :=
   eapply [ "EApply" constrarg_binding_list($cl) ]
       -> [(EApplyWithBindings ($LIST $cl))]
 | eexact [ "EExact" constrarg($c) ] -> [(EExact $c)]
diff --git a/tactics/Equality.v b/tactics/Equality.v
index 1cbf506270..95739e8388 100644
--- a/tactics/Equality.v
+++ b/tactics/Equality.v
@@ -3,41 +3,41 @@
 
 Declare ML Module "equality".
 
-Grammar vernac orient_rule:=
-   lr ["LR"] -> ["LR"]
-  |rl ["RL"] -> ["RL"]
-with rule_list: List :=
+Grammar vernac orient_rule: Ast :=
+   lr ["LR"] -> [ "LR" ]
+  |rl ["RL"] -> [ "RL" ]
+with rule_list: AstList :=
    single_rlt [ constrarg($com) orient_rule($ort) ] ->
-     [(VERNACARGLIST $com $ort)]
+     [ (VERNACARGLIST $com $ort) ]
   |recursive_rlt [ constrarg($com) orient_rule($ort) rule_list($tail)] ->
-    [(VERNACARGLIST $com $ort) ($LIST $tail)]
-with base_list: List :=
+    [ (VERNACARGLIST $com $ort) ($LIST $tail) ]
+with base_list: AstList :=
    single_blt [identarg($rbase) "[" rule_list($rlt) "]"] ->
-     [(VERNACARGLIST $rbase ($LIST $rlt))]
+     [ (VERNACARGLIST $rbase ($LIST $rlt)) ]
   |recursive_blt [identarg($rbase) "[" rule_list($rlt) "]"
     base_list($blt)] ->
-    [(VERNACARGLIST $rbase ($LIST $rlt)) ($LIST $blt)]
-with vernac:=
+    [ (VERNACARGLIST $rbase ($LIST $rlt)) ($LIST $blt) ]
+with vernac: Ast :=
    addrule ["HintRewrite" base_list($blt) "."] ->
-     [(HintRewrite ($LIST $blt))].
+     [ (HintRewrite ($LIST $blt)) ].
 
-Grammar tactic list_tactics: List :=
+Grammar tactic list_tactics: AstList :=
    single_lt [tactic($tac)] -> [$tac]
   |recursive_lt [tactic($tac) "|" list_tactics($tail)] ->
-    [$tac ($LIST $tail)]
+    [ $tac ($LIST $tail) ]
 
-with step_largs: List :=
+with step_largs: AstList :=
    nil_step [] -> []
   |solve_step ["with" "Solve"] -> [(REDEXP (SolveStep))]
   |use_step ["with" "Use"] -> [(REDEXP (Use))]
   |all_step ["with" "All"] -> [(REDEXP (All))]
 
-with rest_largs: List :=
+with rest_largs: AstList :=
    nil_rest [] -> []
   |solve_rest ["with" "Solve"] -> [(REDEXP (SolveRest))]
   |cond_rest ["with" "Cond"] -> [(REDEXP (Cond))]
 
-with autorew_largs: List :=
+with autorew_largs: AstList :=
    step_arg ["Step" "=" "[" list_tactics($ltac) "]" step_largs($slargs)] ->
     [(REDEXP (Step ($LIST $ltac))) ($LIST $slargs)]
   |rest_arg ["Rest" "=" "[" list_tactics($ltac) "]" rest_largs($llargs)] ->
@@ -45,30 +45,30 @@ with autorew_largs: List :=
   |depth_arg ["Depth" "=" numarg($dth)] ->
     [(REDEXP (Depth $dth))]
 
-with list_args_autorew: List :=
+with list_args_autorew: AstList :=
    nil_laa [] -> []
   |recursive_laa [autorew_largs($largs) list_args_autorew($laa)] ->
     [($LIST $largs) ($LIST $laa)]
 
-with hintbase_list: List :=
+with hintbase_list: AstList :=
   nil_hintbase [] -> []
 | base_by_name [identarg($id) hintbase_list($tail)] -> 
        [ (REDEXP (ByName $id)) ($LIST $tail)]
 | explicit_base ["[" hintbase($b) "]" hintbase_list($tail)] -> 
        [(REDEXP (Explicit ($LIST $b))) ($LIST $tail) ]
 
-with hintbase: List := 
+with hintbase: AstList := 
   onehint_lr [ constrarg($c) "LR" ] -> [(REDEXP (LR $c))]
 | onehint_rl  [ constrarg($c) "RL" ] -> [(REDEXP (RL $c))]
 | conshint_lr [ constrarg($c) "LR" hintbase($tail)] -> [(REDEXP (LR $c)) ($LIST $tail)]
 | conshint_rl [ constrarg($c) "RL" hintbase($tail)] -> [(REDEXP (RL $c)) ($LIST $tail)]
 
-with simple_tactic := 
+with simple_tactic: Ast := 
  AutoRewrite [ "AutoRewrite" "[" hintbase_list($lbase) "]"
   list_args_autorew($laa)] ->
   [(AutoRewrite (REDEXP (BaseList ($LIST $lbase))) ($LIST $laa))].
 
-Grammar tactic simple_tactic :=
+Grammar tactic simple_tactic: Ast :=
   replace [ "Replace" constrarg($c1) "with" constrarg($c2) ] -> [(Replace $c1 $c2)]
 
 | deqhyp   [ "Simplify_eq" identarg($id) ] -> [(DEqHyp $id)]
diff --git a/tactics/Inv.v b/tactics/Inv.v
index 544232c400..d2df140e5f 100644
--- a/tactics/Inv.v
+++ b/tactics/Inv.v
@@ -26,7 +26,7 @@ Syntax tactic level 0:
 | inversion_clear  [(INVCOM InversionClear)] -> [ "Inversion_clear" ].
 
 
-Grammar tactic simple_tactic :=
+Grammar tactic simple_tactic: Ast :=
   inversion    [ inversion_com($ic) identarg($id) ] -> [(Inv $ic $id)]
 | inversion_in [ inversion_com($ic) identarg($id) "in" ne_identarg_list($l) ]
       -> [(InvIn $ic $id ($LIST $l))]
@@ -48,13 +48,13 @@ Grammar tactic simple_tactic :=
           Inversion -> [(UseInversionLemmaIn $id $c ($LIST $l))]
         esac
 
-with inversion_com :=
+with inversion_com: Ast :=
   simple_inv    [ "Simple" "Inversion" ] -> [ HalfInversion ]
 | inversion_com [ "Inversion" ] -> [ Inversion ]
 | inv_clear     [ "Inversion_clear" ] -> [ InversionClear ].
 
 
-Grammar vernac vernac :=
+Grammar vernac vernac: Ast :=
   der_inv_clr [ "Derive" "Inversion_clear"  identarg($na) identarg($id) "." ]
                -> [(MakeInversionLemmaFromHyp 1 $na $id)]
 
diff --git a/tactics/Tauto.v b/tactics/Tauto.v
index 2f7cbb0eac..40a4a048b6 100644
--- a/tactics/Tauto.v
+++ b/tactics/Tauto.v
@@ -3,7 +3,7 @@
 
 Declare ML Module "Tauto".
 
-Grammar tactic simple_tactic :=
+Grammar tactic simple_tactic: Ast :=
   tauto [ "Tauto" ] -> [(Tauto)]
 | intuition [ "Intuition" ] -> [(Intuition)].
 
diff --git a/theories/Init/DatatypesSyntax.v b/theories/Init/DatatypesSyntax.v
index 520c988d24..fb6476e7ea 100644
--- a/theories/Init/DatatypesSyntax.v
+++ b/theories/Init/DatatypesSyntax.v
@@ -7,18 +7,18 @@ Require Export Datatypes.
 
 Grammar constr constr1 :=
   pair_expl [ "<" lconstr($l1) "," lconstr($c2) ">" "(" lconstr($c3) ","
-    lconstr($c4) ")" ] -> [<<(pair $l1 $c2 $c3 $c4)>>]
+    lconstr($c4) ")" ] -> [ (pair $l1 $c2 $c3 $c4) ]
 | fst_expl [ "<" lconstr($l1) "," lconstr($c2) ">" "Fst" "("
-    lconstr($l) ")" ] -> [<<(fst $l1 $c2 $l)>>]
+    lconstr($l) ")" ] -> [ (fst $l1 $c2 $l) ]
 | snd_expl [ "<" lconstr($l1) "," lconstr($c2) ">" "Snd" "("
-    lconstr($l) ")" ] -> [<<(snd $l1 $c2 $l)>>]
+    lconstr($l) ")" ] -> [ (snd $l1 $c2 $l) ]
 
 with constr0 :=
   pair [ "(" lconstr($lc1) "," lconstr($lc2) ")" ] ->
-         [<<(pair ? ? $lc1 $lc2)>>]
+         [ (pair ? ? $lc1 $lc2) ]
 
 with constr3 :=
-  prod [ constr2($c1) "*" constr3($c2) ] -> [<<(prod $c1 $c2)>>].
+  prod [ constr2($c1) "*" constr3($c2) ] -> [ (prod $c1 $c2) ].
 
 (* Pretty-printing of things in Datatypes.v *)
 
diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v
index 50bed88279..57b76e0176 100644
--- a/theories/Init/LogicSyntax.v
+++ b/theories/Init/LogicSyntax.v
@@ -7,44 +7,44 @@ Require Export Logic.
 
 Grammar constr constr1 :=
   conj [ "<" lconstr($l1) "," lconstr($c2) ">" "{" constr($c3) ","
-        constr($c4) "}" ] -> [<<(conj $l1 $c2 $c3 $c4)>>]
+        constr($c4) "}" ] -> [ (conj $l1 $c2 $c3 $c4) ]
 | proj1 [ "<" lconstr($l1) "," lconstr($c2) ">" "Fst" "{"
-        lconstr($l) "}" ] -> [<<(proj1 $l1 $c2 $l)>>]
+        lconstr($l) "}" ] -> [ (proj1 $l1 $c2 $l) ]
 | proj2 [ "<" lconstr($l1) "," lconstr($c2) ">" "Snd" "{"
-        lconstr($l) "}" ] -> [<<(proj2 $l1 $c2 $l)>>]
+        lconstr($l) "}" ] -> [ (proj2 $l1 $c2 $l) ]
 | IF [ "either" constr($c) "and_then" constr($t) "or_else" constr($e) ] ->
-       [<<(IF $c $t $e)>>]
+       [ (IF $c $t $e) ]
 | all [ "<" lconstr($l1) ">" "All" "(" lconstr($l2) ")" ] ->
-       [<<(all $l1 $l2)>>]
+       [ (all $l1 $l2) ]
 | eq_expl [ "<" lconstr($l1) ">" constr0($c1) "=" constr0($c2) ] ->
-            [<<(eq $l1 $c1 $c2)>>]
-| eq_impl [ constr0($c) "=" constr0($c2) ] -> [<<(eq ? $c $c2)>>]
+            [ (eq $l1 $c1 $c2) ]
+| eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eq ? $c $c2) ]
 
 with constr2 :=
-  not [ "~" constr2($c) ] -> [<<(not $c)>>]
+  not [ "~" constr2($c) ] -> [ (not $c) ]
 
 with constr6 :=
-  and [ constr5($c1) "/\\" constr6($c2) ] -> [<<(and $c1 $c2)>>]
+  and [ constr5($c1) "/\\" constr6($c2) ] -> [ (and $c1 $c2) ]
 
 with constr7 :=
-  or [ constr6($c1) "\\/" constr7($c2) ] -> [<<(or $c1 $c2)>>]
+  or [ constr6($c1) "\\/" constr7($c2) ] -> [ (or $c1 $c2) ]
 
 with constr8 :=
-  iff [ constr7($c1) "<->" constr8($c2) ] -> [<<(iff $c1 $c2)>>]
+  iff [ constr7($c1) "<->" constr8($c2) ] -> [ (iff $c1 $c2) ]
 
 with constr10 :=
   allexplicit [ "ALL" ident($x) ":" constr($t) "|" constr($p) ]
-                          -> [<<(all $t [$x : $t]$p)>>]
+                          -> [ (all $t [$x : $t]$p) ]
 | allimplicit [ "ALL" ident($x) "|" constr($p) ]
-                          -> [<<(all ? [$x]$p)>>]
+                          -> [ (all ? [$x]$p) ]
 | exexplicit [ "EX" ident($v) ":" constr($t) "|" constr($c1) ]
-                          -> [<<(ex $t [$v : $t]$c1)>>]
+                          -> [ (ex $t [$v : $t]$c1) ]
 | eximplicit [ "EX" ident($v) "|" constr($c1) ] 
-                          -> [<<(ex ? [$v]$c1)>>]
+                          -> [ (ex ? [$v]$c1) ]
 | ex2explicit [ "EX" ident($v) ":" constr($t) "|" constr($c1) "&"
-           constr($c2) ] -> [<<(ex2 $t [$v : $t]$c1 [$v : $t]$c2)>>]
+           constr($c2) ] -> [ (ex2 $t [$v : $t]$c1 [$v : $t]$c2) ]
 | ex2implicit [ "EX" ident($v) "|" constr($c1) "&" 
-           constr($c2) ] -> [<<(ex2 ? [$v]$c1 [$v]$c2)>>].
+           constr($c2) ] -> [ (ex2 ? [$v]$c1 [$v]$c2) ].
 
 
 (* Pretty-printing of things in Logic.v *)
diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v
index 8b467fe13f..a3a69c3100 100644
--- a/theories/Init/SpecifSyntax.v
+++ b/theories/Init/SpecifSyntax.v
@@ -8,20 +8,21 @@ Require Export Specif.
 
 Grammar constr constr1 :=
   sig [ "{" lconstr($lc) ":" lconstr($c1) "|" lconstr($c2) "}" ]
-       -> [<<(sig $c1 [$lc : $c1]$c2)>>]
+       -> [ (sig $c1 [$lc : $c1]$c2) ]
 
 | sig2 [ "{" lconstr($lc) ":" lconstr($c1)
            "|" lconstr($c2) "&" lconstr($c3) "}" ]
-       -> [<<(sig2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3)>>]
+       -> [ (sig2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3) ]
 
 | sigS [ "{" lconstr($lc) ":" lconstr($c1) "&" lconstr($c2) "}" ]
-       -> [<<(sigS $c1 [$lc : $c1]$c2)>>]
+       -> [ (sigS $c1 [$lc : $c1]$c2) ]
 
 | sigS2 [ "{" lconstr($lc) ":" lconstr($c1)
              "&" lconstr($c2) "&" lconstr($c3) "}" ]
-       -> [<<(sigS2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3)>>]
+       -> [ (sigS2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3) ].
 
-| squash [ "{" lconstr($lc) "}" ] -> [(SQUASH $lc)].
+Grammar constr constr1: Ast :=
+  squash [ "{" lconstr($lc) "}" ] -> [(SQUASH $lc)].
 
 Grammar constr lassoc_constr4 :=
   squash_sum
@@ -29,10 +30,10 @@ Grammar constr lassoc_constr4 :=
       case [$c2] of
         (SQUASH $T2) ->
             case [$c1] of
-              (SQUASH $T1) -> [<<(sumbool $T1 $T2)>>] (* {T1}+{T2} *)
-            | $_           -> [<<(sumor $c1 $T2)>>]   (* c1+{T2} *)
+              (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *)
+            | $_           -> [ (sumor $c1 $T2) ]   (* c1+{T2} *)
             esac
-      | $_           -> [<<(sum $c1 $c2)>>]           (* c1+c2 *)
+      | $_           -> [ (sum $c1 $c2) ]           (* c1+c2 *)
       esac.
 
 (* Pretty-printing of things in Specif.v *)