pretty-print

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

4 files changed, 659 insertions, 0 deletions

diff --git a/syntax/MakeBare.v b/syntax/MakeBare.v
new file mode 100644
index 000000000..a3fe30035
--- /dev/null
+++ b/syntax/MakeBare.v
@@ -0,0 +1,3 @@
+Load PPCommand.
+Load PPTactic.
+Load PPMultipleCase.
diff --git a/syntax/PPCommand.v b/syntax/PPCommand.v
new file mode 100755
index 000000000..4a39c94c1
--- /dev/null
+++ b/syntax/PPCommand.v
@@ -0,0 +1,220 @@
+
+(* $Id$ *)
+
+(* Syntax for the Calculus of Constructions. *)
+
+Syntax constr
+  level 0:
+    ne_command_listcons [(NECOMMANDLIST $c1 ($LIST $cl))]
+       -> [ $c1 [1 0] (NECOMMANDLIST ($LIST $cl)) ]
+  | ne_command_listone [(NECOMMANDLIST $c1)] -> [ $c1 ]
+  ;
+
+(* Things parsed in binder *)
+(* ======================= *)
+
+  level 0:
+    idbindercons [(IDBINDER ($VAR $id) ($LIST $L))] ->
+       [ $id ","[0 0] (IDBINDER ($LIST $L))]
+  | idbinderone  [(IDBINDER ($VAR $id))] -> [$id]
+  | idbindernil  [(IDBINDER)] -> [ ]
+
+  | 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)))] -> 
+       [ [<hov 0> (IDBINDER ($LIST $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"]
+(* Note: Atomic constants (Nvar, CONST, MUTIND, MUTCONSTRUCT) are printed in
+   typing/printer to deal with the duality CCI/FW *)
+
+  | evar [<< ? >>] -> ["?"]
+  | meta [(META ($NUM $n))] -> [ "?" $n ]
+  | implicit [(IMPLICIT)] -> ["<Implicit>"]
+  ;
+
+(* Things parsed in command1 *)
+  level 1:
+    soap [(XTRA "$SOAPP" $lc1 ($LIST $cl))]
+      -> [ [<hov 0> "(" $lc1 ")@[" (NECOMMANDLIST ($LIST $cl)) "]"] ]
+  | let_K [(ABST #Core#let.cci $M [<>]$N)]
+      -> [ [<hov 0> "[_=" $M "]" [0 1] $N:E ] ]
+
+  | let [<<[$x = $M]$N>>] -> [ [<hov 0> "[" $x "=" $M:E "]" [0 1] $N:E ] ]
+ 
+  | abstpat  [[$id1]$c] -> [ [<hov 0> "<<" $id1 ">>" [0 1] $c:E ] ]
+  ;
+
+(* Things parsed in command2 *)
+
+(* Things parsed in command3 *)
+
+(* Things parsed in command4 *)
+
+(* Things parsed in command5 *)
+
+  level 5:
+    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 $Body)]
+     -> [(LAMBOX (BINDERS) (LAMBDA $Dom $Body))]
+  | lambdalist  [(LAMBDALIST $c $body)]
+     -> [(LAMBOX (BINDERS) (LAMBDALIST $c $body))]
+
+  | formated_lambda [(LAMBOX $pbi $t)]
+     -> [ [<hov 0> "[" [<hv 0> $pbi] "]" [0 1] $t:E ] ]
+
+  | lambda_cons [(LAMBOX (BINDERS ($LIST $acc)) <<[$x : $Dom]$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))]
+      -> [(LAMLBOX $pbi $Dom (IDS) $Body)]
+
+  | 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)]
+      -> [(LAMLBOX $pbi $c (IDS ($LIST $ids) _) $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)]
+       -> [(PRODBOX (BINDERS) (PRODLIST $c $b))]
+
+  | formated_prod [(PRODBOX $pbi $t)]
+     -> [ [<hov 0> "(" [<hov 0> $pbi] ")" [0 1] $t:E ] ]
+
+  | prod_cons [(PRODBOX (BINDERS ($LIST $acc)) <<($x : $Dom)$body>>)]
+      -> [(PRODBOX (BINDERS ($LIST $acc) (BINDER $Dom $x)) $body)]
+  | prodl_start [(PRODBOX $pbi (PRODLIST $Dom $Body))]
+      -> [(PRODLBOX $pbi $Dom (IDS) $Body)]
+
+  | 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)]
+      -> [(PRODLBOX $pbi $c (IDS ($LIST $ids) _) $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)]
+  ;
+
+(* Things parsed in command9 *)
+
+(* Things parsed in command10 *)
+  level 10:
+    app_cons [(APPLIST $H ($LIST $T))]
+                 -> [ [<hov 0>  $H:E  (APPTAIL ($LIST $T)):E ] ]
+
+  | app_imp  [(APPLIST (XTRA "!" $H) ($LIST $T))]
+                 -> [ (APPLISTIMPL (ACC $H) ($LIST $T)):E ]
+
+  | app_imp_arg  [(APPLISTIMPL (ACC ($LIST $AC)) $a ($LIST $T))]
+        -> [ (APPLISTIMPL (ACC ($LIST $AC) $a) ($LIST $T)):E ]
+
+  | app_imp_imp_arg  [ (APPLISTIMPL $AC (XTRA "!" $_ $_) ($LIST $T)) ]
+       -> [ (APPLISTIMPL $AC ($LIST $T)):E ]
+
+  | 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 (XTRA "!" $n $c1) ($LIST $T))]
+         -> [ [1 1] (XTRA "!" $n $c1):L  (APPTAIL ($LIST $T)):E ]
+  ;
+
+(* Implicits *)
+  level 8:
+    arg_implicit [(XTRA "!" ($NUM $n) $c1)] -> [ $n "!" $c1:L ]
+  | arg_implicit1 [(XTRA "!" "EX" ($NUM $n) $c1)] -> [ $n "!" $c1:L ]
+  | fun_explicit [(XTRA "!" $f)] -> [ $f ]
+  ;
+
+
+  level 8:
+    recpr [(XTRA "REC" ($LIST $RECARGS))] -> [ (RECTERM ($LIST $RECARGS)) ]
+
+  | 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))]
+       -> [ (MLCASETERM ($LIST $RECARGS)) ]
+
+  | 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))]
+       -> [ (MLMATCHTERM ($LIST $RECARGS)) ]
+
+  | 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))]
+       -> [ [<hov 0> [<hov 0> $B:E ] FNL] (MATCHBRANCHES ($LIST $T)):E ]
+  | matchbranchesnil [(MATCHBRANCHES)] -> [ ]
+
+  | 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))] ->
+      [ [<hov 0> "Fix " $f
+           [0 2] "{" [<v 0> [<hov 0> $def]
+                            (FIXDECLS ($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))] ->
+      [ FNL [<hov 0> "with " $def1] (FIXDECLS ($LIST $defs)) ]
+  ;
+
+  level 8:
+    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)] ->
+      [ $f
+        [1 2] "[" [<hv 0> (BINDERS ($LIST $l))] "]"
+        [1 2] ": " $A:E " :="
+        [1 2] $t:E ]
+  | onecofixdecl [(CFDECL $f $A $t)] ->
+      [ $f " : "
+        [1 2] $A:E " :="
+        [1 2] $t:E ].
diff --git a/syntax/PPMultipleCase.v b/syntax/PPMultipleCase.v
new file mode 100755
index 000000000..51f75569e
--- /dev/null
+++ b/syntax/PPMultipleCase.v
@@ -0,0 +1,106 @@
+(****************************************************************************)
+(*                 The Calculus of Inductive Constructions                  *)
+(*                                                                          *)
+(*                                Projet Coq                                *)
+(*                                                                          *)
+(*                     INRIA                        ENS-CNRS                *)
+(*              Rocquencourt                        Lyon                    *)
+(*                                                                          *)
+(*                                Coq V5.10                                 *)
+(*                              Nov 25th 1994                               *)
+(*                                                                          *)
+(****************************************************************************)
+(*                             PPMutilpleCase.v                             *)
+(****************************************************************************)
+
+
+Syntax constr
+  level 0:
+    ne_command_listcons2 [(NECOMMANDLIST2 $c1 ($LIST $cl))]
+      -> [ $c1:L [1 0] (NECOMMANDLIST2 ($LIST $cl)) ]
+  | ne_command_listone2 [(NECOMMANDLIST2 $c1)] -> [$c1:L]
+  ;
+
+  level 10:
+    as_patt [(XTRA "AS" $var $patt)] -> [$patt:L" as "$var]
+  ;
+
+  level 0:
+    ne_pattlist_nil  [(PATTLIST)] -> [ ]
+  | ne_pattlist_cons [(PATTLIST $patt ($LIST $lpatt))]
+      -> [$patt:E " " (PATTLIST ($LIST $lpatt))]
+  ;
+
+  level 8:
+    equation [(XTRA "EQN" $rhs ($LIST $lhs))]
+      -> [ [<hov 0> (PATTLIST ($LIST $lhs)) "=> " [0 1] $rhs:E] ]
+  | lam_eqn [(XTRA "LAMEQN" $eq)] -> [ $eq ]
+  | lam_eqn_var [(XTRA "LAMEQN" ($ID $id) ($LIST $l))]
+      -> [(XTRA "LAMEQN" ($LIST $l))]
+  | lam_eqn_dlam      [(XTRA "LAMEQN" [$_]$eq)] -> [(XTRA "LAMEQN" $eq)]
+  | lam_eqn_dlam_anon [(XTRA "LAMEQN" [<>]$eq)] -> [(XTRA "LAMEQN" $eq)]
+  ;
+ 
+  level 0:
+    bar_eqnlist_nil [(BAREQNLIST)] -> [ ]
+  | bar_eqnlist_cons [(BAREQNLIST $eqn ($LIST $leqn))]
+      -> [ "| " $eqn [1 0] (BAREQNLIST ($LIST $leqn)) ]
+  | bar_eqnlist_one [(BAREQNLIST $eqn)]
+      -> [ "| " $eqn ]
+
+  | tomatch [(XTRA "TOMATCH" ($LIST $lc))] -> [(NECOMMANDLIST2 ($LIST $lc)):E]
+  ;
+
+  level 8:
+
+    cases_exp_none [(XTRA "MULTCASE" $pred $tomatch)]
+      -> [ [<hov 0> (ELIMPRED $pred)
+              [<hv 0> "Cases"[1 2] $tomatch:E [1 0] "of"] [1 0] "end"] ]
+
+  | cases_exp_one [(XTRA "MULTCASE" $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 [(XTRA "MULTCASE" $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]
+                     (BAREQNLIST $eqn2 ($LIST $eqns)) [1 0]
+                     "end"] ] ]
+
+  (* "level" indifférent pour ce qui suit *)
+  | let_binder_var [(LETBINDER ($VAR $id))] -> [ $id ]
+  | let_binder_app [(LETBINDER (APPLIST $toforget ($VAR $id) ($LIST $vars)))]
+      -> [ "(" $id (LETBINDERTAIL ($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 (XTRA"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 $c1 $c2)]
+      -> [ [<hov 0> (ELIMPRED $pred)
+              [<hv 0> "if " [<hov 0> $tomatch:E ]
+                      [1 0] [<hov 0> "then" [1 1] $c1:E ]
+                      [1 0] [<hov 0> "else" [1 1] $c2:E ] ] ] ]
+
+  (* Tiens ! 
+  Pourquoi l'AST n'est pas (FORCELET $pred tomatch (EQN $c $pat)) ? 
+  Réponse : FORCELET, c'est par commodité, EQN, c'est parce qu'au parsing
+  il y a un XTRA devant **)
+
+
+  | let_cases [(XTRA "FORCELET" $pred $tomatch (XTRA "EQN" $c $pat))]
+      -> [ [<hov 0> (ELIMPRED $pred)
+              [<hv 0> "let " [<hov 0> (LETBINDER $pat) ] " ="
+                      [1 1] [<hov 0> $tomatch:E ] ]
+              [1 0] "in " [<hov 0> $c:E ] ] ]
+.
diff --git a/syntax/PPTactic.v b/syntax/PPTactic.v
new file mode 100644
index 000000000..e97df073f
--- /dev/null
+++ b/syntax/PPTactic.v
@@ -0,0 +1,330 @@
+(****************************************************************************)
+(*                 The Calculus of Inductive Constructions                  *)
+(*                                                                          *)
+(*                                Projet Coq                                *)
+(*                                                                          *)
+(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
+(*              Rocquencourt         Orsay          Lyon                    *)
+(*                                                                          *)
+(*                                 Coq V6.3                                 *)
+(*                               July 1st 1999                              *)
+(*                                                                          *)
+(****************************************************************************)
+(*                                PPTactic.v                                *)
+(****************************************************************************)
+
+(* ======================================= *)
+(*   PP rules for basic elements           *)
+(* ======================================= *)
+
+Syntax tactic
+  level 3:
+    interpret [(Interpret (TACTIC $t))] -> [ $t:E ]
+  ;
+
+  (* Put parenthesis when there is more than one tactic *)
+  level 3:
+    tacsemilist_many [(TACTICLIST ($LIST $L))]
+      -> [ [ <hov 2> (TACTICS ($LIST $L)) ] ]
+  ;
+
+  level 2:
+    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] ]
+
+  | tactic_seq [(TACLIST ($LIST $l))]
+             -> [ [<hv 0> "[ " (TACTICSEQBODY ($LIST $l)) " ]" ] ]
+
+  | tacticseqbody_cons [(TACTICSEQBODY $t ($LIST $l))]
+      -> [ [<hov 0> $t] [1 0] "| " (TACTICSEQBODY ($LIST $l)) ]
+  | tacticseqbody_one  [(TACTICSEQBODY $t)] -> [ [<hov 0> $t] ]
+  ;
+
+  level 1:
+    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))] ->
+    ["First" [1 0] "[" [1 0] (TACTICSEQBODY ($LIST $l)) [1 0] "]"]
+  | solve  [(TCLSOLVE ($LIST $l))] ->
+    ["Solve" [1 0] "[" [1 0] (TACTICSEQBODY ($LIST $l)) [1 0] "]"]
+
+  | call [(CALL $macro ($LIST $args))]
+         -> [ [<hv 3> $macro " " (LISTSPC ($LIST $args)) ] ] 
+  | abstract_anon [(ABSTRACT (TACTIC $t))] 
+         -> ["Abstract " $t:E]
+  | 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 ]
+
+  | split [(Split $b)] -> [ "Split" (WITHBINDING $b) ]
+  | exists [(Exists $b)] -> ["Exists" $b] (* unused! *)
+
+  | 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))] ->
+	[ "Auto" [1 0] $n [1 0] "with " [<hov 0> (LISTSPC ($LIST $lid))] ]
+  | auto [(Auto)] -> ["Auto"]
+
+  | 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"]
+
+  | 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"]
+
+  | apply [(Apply $c $b)] -> ["Apply " $c (WITHBINDING $b)]
+
+  | oldelim [(Elim1 $C)] -> ["OldElim " $C]
+
+  | 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]
+
+  | case_tac [(Case $c $b)] -> ["Case " $c (WITHBINDING $b) ]
+
+  | 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 " $n " " $c (WITHBINDING $b) ]
+
+  | generalize [(Generalize ($LIST $lc))]
+      -> [ [<hov 3> "Generalize " (LISTSPC ($LIST $lc))] ]
+
+  | lapply [(CutAndApply $c)] -> ["LApply " $c]
+
+  | clear [(Clear (CLAUSE ($LIST $l)))] ->
+          [ [<hov 3> "Clear " (LISTSPC ($LIST $l))] ]
+
+  | move [(MoveDep $id1 $id2)] ->
+          [ "Move " $id1 " after " $id2 ]
+
+  | constructor [(Constructor)] -> ["Constructor" ]
+  | constructor_num [(Constructor ($NUM $n) $b)]
+      -> ["Constructor " $n (WITHBINDING $b) ]
+
+  | trivial [(Trivial)] -> ["Trivial"]
+
+  | failingtrivial [(FailingTrivial)] -> ["Trivial"]
+
+  | inductionid [(Induction $id)] -> ["Induction " $id]
+  | inductionnum [(Induction ($NUM $n))] -> ["Induction " $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 )] -> 
+              ["Decompose" [1 1] [<hov 0> "[" (LISTSPC ($LIST $l)) "]" ] 
+	                         [1 1] $c]
+  | 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 ]
+
+  | 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 ]
+
+  | fixdeclcons [(FIXLIST $cfe ($LIST $fd))]
+      -> [ [1 0] $cfe (FIXLIST ($LIST $fd))]
+  | fixdeclnil  [(FIXLIST)] -> [ ]
+
+  | exact [(Exact $C)] -> ["Exact " $C]
+
+  | absurd [(Absurd $C)] -> ["Absurd " $C]
+
+  | cut [(Cut $C)] -> ["Cut " $C]
+  | lettac [(LetTac $id $c (LETPATTERNS ($LIST $pl)))] -> 
+	["Let" [1 1] $id ":=" $c [1 1] "in" [1 1] (LETPATTERNS ($LIST $pl))]
+
+  | left [(Left $b)] -> ["Left" (WITHBINDING $b)]
+  | right [(Right $b)] -> [ "Right" (WITHBINDING $b)]
+
+  | discriminate [(Discriminate)] -> ["Simple Discriminate"]
+
+  | reflexivity [(Reflexivity)] -> ["Reflexivity"]
+  | symmetry [(Symmetry)] -> ["Symmetry"]
+  | transitivity [(Transitivity $C)] -> ["Transitivity " $C]
+
+  | idtac [(Idtac)] -> ["Idtac"]
+
+
+(* ============================================== *)
+(*      PP rules for tactic arguments             *)
+(* ============================================== *)
+
+  | idargnil [(IDARGLIST)] -> [ ]
+  | idargcons
+      [(IDARGLIST $id ($LIST $L))] -> [ $id " "  (IDARGLIST ($LIST $L)) ]
+
+  | nenumlistcons
+      [(NENUMLIST ($NUM $n) ($LIST $l))] -> [ $n " " (NENUMLIST ($LIST $l)) ]
+  | nenumlistone [(NENUMLIST ($NUM $n))] -> [ $n ]
+
+  | numlistcons [(NUMLIST ($LIST $l))] -> [ (NENUMLIST ($LIST $l)) ]
+  | numlistnil [(NUMLIST)] -> [ ]
+
+  (* Bindings: print "with" before the bindings. *)
+  | with_binding [(WITHBINDING (BINDINGS ($LIST $b)))]
+       -> [ [1 1] "with " [<hov 0> (BINDBOX ($LIST $b)) ] ]
+  | without_binding [(WITHBINDING (BINDINGS))] -> [ ]
+
+  (* Bindings: nor break nor "with" before. *)
+  | 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))]
+      -> [ $b [1 0] (BINDBOX ($LIST $bl)) ]
+  | 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)))] ->
+       [ [<hv 3> "Unfold " (UNFOLDLIST ($LIST $unf))] ]
+  | 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)))] ->
+       [ [<hv 3> "Pattern " (NEPATTERNLIST ($LIST $pl)) ] ]
+
+  | flags_beta [(FLAGS (Beta) ($LIST $F))] ->
+        [ [1 0] "Beta" (FLAGS ($LIST $F))]
+  | flags_delta [(FLAGS (Delta) ($LIST $F))] ->
+        [ [1 0] "Delta" (FLAGS ($LIST $F))]
+  | flags_iota [(FLAGS (Iota) ($LIST $F))] ->
+        [ [1 0] "Iota" (FLAGS ($LIST $F))]
+  | delta_unf [(FLAGS (Unf ($LIST $idl)))]
+         -> [ [1 0] "[" [<hov 0> (LISTSPC ($LIST $idl)) ] "]" ]
+  | delta_unfbut [(FLAGS (UnfBut ($LIST $idl)))]
+         -> [ [1 0] "-[" [<hov 0> (LISTSPC ($LIST $idl)) ] "]" ]
+  | flags_nil [(FLAGS)] -> [ ]
+
+
+  | unfoldcons
+        [(UNFOLDLIST $H ($LIST $T))] -> [ $H " " (UNFOLDLIST ($LIST $T)) ]
+  | unfoldone [(UNFOLDLIST $H)] -> [ $H ]
+
+  | unfoldarg [(UNFOLD $id ($LIST $OCCL))]
+         -> [ (UNFOLDOCCLIST ($LIST $OCCL)) (COMMAND $id) ]
+
+  | 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)))] -> 
+                      ["Adding" [1 1] "[" (LISTSPC ($LIST $l)) "]"]
+
+  | autoarg_adding2     [(AUTOARG (CLAUSE))] -> [""]
+  | autoarg_destructing [(AUTOARG "Destructing")] -> 
+                        ["Destructing"]
+  | autoarg_usingTDB    [(AUTOARG "UsingTDB")]    -> ["Using TDB"]
+  | autoarg_noarg       [(AUTOARG "NoAutoArg")]   -> [""]
+  
+  | intropatlist [(LISTPATTERN ($LIST $tl))] ->
+                 [ (LISTSPC ($LIST $tl)) ]
+  | intropatdisj [(DISJPATTERN ($LIST $dp))] ->
+                 [ "[" [<hv 0> (LISTBAR ($LIST $dp))] "]" ]
+  | intropatconj [(CONJPATTERN ($LIST $cp))] ->
+                 [ "(" [<hov 0> (LISTCOMA ($LIST $cp))] ")" ]
+  | intropatid [(IDENTIFIER ($VAR $id))] -> [ $id ]
+
+
+  | patterncons [(NEPATTERNLIST $H ($LIST $T))]
+         -> [ [<hov 1> $H ] [1 0] (NEPATTERNLIST ($LIST $T)) ]
+  | patternone [(NEPATTERNLIST $H)] -> [ [<hov 1> $H ] ]
+
+  | patternargoccs [(PATTERN $c ($LIST $OCCL))]
+         -> [ [<hov 1> (NENUMLIST ($LIST $OCCL)) ] [1 1] $c ]
+  | patternargnil [(PATTERN $c)] -> [ $c ]
+
+
+  | letpatterncons [(LETPATTERNS $H ($LIST $T))]
+         -> [ [<hov 1> $H ] [1 0] (LETPATTERNS ($LIST $T)) ]
+  | letpatternone [(LETPATTERNS $H)] -> [ [<hov 1> $H ] ]
+
+  | hyppatternargoccs [(HYPPATTERN $s ($LIST $OCCL))]
+         -> [ [<hov 1> (NENUMLIST ($LIST $OCCL)) ] [1 1] $s ]
+  | hyppatternargnil [(HYPPATTERN $s)] -> [ $s ]
+
+  | cclpatternargoccs [(CCLPATTERN ($LIST $OCCL))]
+         -> [ [<hov 1> (NENUMLIST ($LIST $OCCL)) ] [1 1] "Goal" ]
+  | cclpatternargnil [(CCLPATTERN)] -> [ "Goal" ]
+
+
+  | clause [(CLAUSE ($LIST $l))]
+         -> [ [1 1][<hov 2> "in " (LISTSPC ($LIST $l)) ] ]
+  | clause_none [(CLAUSE)] -> [ ]
+
+
+  (* Lists with separators *)
+  | listspc_cons [(LISTSPC $x ($LIST $l))] ->
+                 [ $x [1 0] (LISTSPC ($LIST $l)) ]
+  | listspc_one  [(LISTSPC $x)] -> [ $x ]
+  | listspc_nil  [(LISTSPC )] -> [ ]
+
+  | listbar_cons [(LISTBAR $x ($LIST $l))] ->
+                 [ $x [1 0]"| " (LISTBAR ($LIST $l)) ]
+  | listbar_one  [(LISTBAR $x)] -> [ $x ]
+  | listbar_nil  [(LISTBAR )] -> [ ]
+
+  | listcoma_cons [(LISTCOMA $x ($LIST $l))] ->
+                  [ $x ","[1 0] (LISTCOMA ($LIST $l)) ]
+  | listcoma_one  [(LISTCOMA $x)] -> [ $x ]
+  | listcoma_nil  [(LISTCOMA )] -> [ ]
+  ;
+
+  level 8:
+  command [(COMMAND $c)] -> [ (PPUNI$COMMAND $c):E ].
+
+
+(* $Id$ *)