syntax/PPTactic.v passe au niveau ML

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

1 files changed, 0 insertions, 450 deletions

diff --git a/syntax/PPTactic.v b/syntax/PPTactic.v
deleted file mode 100644
index 434590cb8..000000000
--- a/syntax/PPTactic.v
+++ /dev/null
@@ -1,450 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(* $Id$ *)
-
-Syntax tactic
-
-(* ======================================== *)
-(*     PP rules for the tactic language     *)
-(* ======================================== *)
-
-  level 4:
-  | interpret [<<(Interp (TACTIC $t))>>] -> [ $t:E ]
-  | tacticlist_parsimp [<<(TACTICLISTPAR $tac0 $tac1)>>] ->
-    [ $tac0 ";" [1 0] $tac1]
-  | tacticlist_parcomp [<<(TACTICLISTPAR $tac0 (TACTICLIST $tac1 $tac2))>>]
-    -> [ (TACTICLIST $tac0 (TACTICLIST $tac1 $tac2)) ]
-  ;
-
-  level 3:
-  | tacticlist_simp [<<(TACTICLIST $tac0 $tac1)>>] ->
-    [ $tac0 ";" [1 0] $tac1]
-  | tacticlist_comp [<<(TACTICLIST $tac0 (TACTICLIST $tac1 $tac2))>>] ->
-    [ $tac0 ";" [1 0] [<hov 0> (TACTICLISTPAR $tac1 $tac2):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] ]
-  ;
-
-(* These constructions should be at level 0 but the application cannot be at
-   the same level than the tacticals and must be also at level 2 for some
-   constructions at level 1. To avoid duplications and particular cases, these
-   constructions have been put here and additional but completely fair
-   parentheses (w.r.t. to what has been parsed) are to be expected. *)
-
-  level 2:
-  | orelse [ $st Orelse $tc ] -> [ [<hov 0> $st:L " Orelse" [1 1] $tc:E] ]
-  | match_context [<<(MATCHCONTEXT "RL" ($LIST $lrul))>>] ->
-    [ [ <hov 0> "Match Context With" (MATCHCONTEXTLIST ($LIST $lrul)) ] ]
-  | match [<<(MATCH $t ($LIST $lrul))>>] ->
-    [ [ <hov 0> "Match" [1 0] $t [1 0] "With" (MATCHLIST ($LIST $lrul)) ] ]
-  | fun [<<(FUN (FUNVAR ($LIST $lvar)) $body)>>] ->
-    [ [ <hov 0> "Fun" [1 0] (FUNVAR ($LIST $lvar)) [1 0] "->" [1 0] $body ] ]
-  | let [<<(LET (LETDECL ($LIST $llc)) $u)>>] ->
-    [ [ <hov 0> "Let" [1 0] (LETDECL ($LIST $llc)) [1 0] "In" FNL $u ] ]
-  | rec [<<(REC $rc)>>] -> [ [ <hov 0> "Rec" [1 0] (RECDECL $rc) ] ]
-  | rec_in [<<(REC (RECDECL ($LIST $rc)) $body)>>] ->
-    [ [ <hov 0> "Rec" [1 0] (RECDECL ($LIST $rc)) [1 0] "In" FNL $body ] ]
-  | app_cons [<<(APP $te ($LIST $lte))>>] -> [ $te [1 0] (APP ($LIST $lte)) ]
-  | app_one [<<(APP $te)>>] -> [ $te ]
-  ;
-
-  level 1:
-
-(* Match Context rules *)
-
-  | term [<<(TERM $t)>>] -> [ $t ]
-  | subterm [<<(SUBTERM ($VAR $id) $t)>>] -> [ $id "[" $t "]" ]
-  | match_context_hyps_id [<<(MATCHCONTEXTHYPS ($VAR $id) $t)>>] ->
-    [ $id [1 0] ":" [1 0] $t]
-  | match_context_hyps_ano [<<(MATCHCONTEXTHYPS $t)>>] ->
-    [ "_" [1 0] ":" [1 0] $t]
-  | hyps_cons [<<(HYPS $hyp0 $hyp1 ($LIST $hyps))>>] ->
-    [ $hyp0 ";" [1 0] (HYPS $hyp1 ($LIST $hyps)) ]
-  | hyps_three [<<(HYPS $hyp $concl $tac)>>] ->
-    [ $hyp [1 0] "|-" [1 0] $concl [1 0] "]" [1 0] "->" [1 2] $tac ]
-  | hyps_two [<<(HYPS $concl $tac)>>] ->
-    [ "|-" [1 0] $concl [1 0] "]" [1 0] "->" [1 2] $tac ]
-  | match_context_rule [<<(MATCHCONTEXTRULE ($LIST $hyps))>>] ->
-    [ "[" [1 0] (HYPS ($LIST $hyps)) ]
-  | match_context_rule_cons [<<(MATCHCONTEXTLIST $rul ($LIST $lrul))>>] ->
-    [ FNL "|" [1 0] $rul (MATCHCONTEXTLIST ($LIST $lrul)) ]
-  | match_context_rule_one [<<(MATCHCONTEXTLIST $rul)>>] ->
-    [ FNL "|" [1 0] $rul ]
-
-(* Match rules *)
-
-  | match_list_cons [<<(MATCHLIST $rul ($LIST $lrul))>>] ->
-    [ $rul (MATCHLIST ($LIST $lrul)) ]
-  | match_list_one [<<(MATCHLIST $rul)>>] -> [ $rul ]
-  | match_rul_pat [<<(MATCHRULE $pat $tac)>>] ->
-    [ FNL "|" [1 0] "[" [1 0] $pat [1 0] "]" [1 0] "->" [1 2] $tac ]
-  | match_rul_all [<<(MATCHRULE $tac)>>] ->
-    [ FNL "|" [1 0] "_" [1 0] "->" [1 2] $tac ]
-
-(* Fun clauses *)
-
-  | fun_var_cons [<<(FUNVAR $var ($LIST $lvar))>>] ->
-    [ $var [1 0] (FUNVAR ($LIST $lvar)) ]
-  | fun_var_one [<<(FUNVAR $var)>>] -> [ $var ]
-  | void [<<(VOID)>>] -> [ "()" ]
-
-(* Let clauses *)
-
-  | let_decl_cons [<<(LETDECL (LETCLAUSE ($LIST $rul)) ($LIST $lrul))>>] ->
-    [ (LET ($LIST $rul)) (LETLIST ($LIST $lrul)) ]
-  | let_decl_one [<<(LETDECL (LETCLAUSE ($LIST $rul)))>>] ->
-    [ (LET ($LIST $rul)) ]
-  | let_list_cons [<<(LETLIST (LETCLAUSE ($LIST $rul)) ($LIST $lrul))>>] ->
-    [ (AND ($LIST $rul)) (LETLIST ($LIST $lrul)) ]
-  | let_list_one [<<(LETLIST (LETCLAUSE ($LIST $rul)))>>] ->
-    [ (AND ($LIST $rul)) ]
-  | let_rule [<<(LET ($VAR $id) $tac)>>] ->
-    [ $id [1 0] "=" [1 0] $tac:E ]
-  | and_rule [<<(AND ($VAR $id) $tac)>>] ->
-    [ FNL "And" [1 0] $id [1 0] "=" [1 0] $tac:E ]
-
-(* Rec clauses *)
-
-  | rec_decl_cons [<<(RECDECL (RECCLAUSE $id (FUNVAR ($LIST $lvar))
-                     $body) ($LIST $lrc))>>] ->
-    [ $id [1 0 ] (FUNVAR ($LIST $lvar)) [1 0] "->" [1 0] $body:E FNL "And"
-      [1 0] (RECDECL ($LIST $lrc)) ]
-  | rec_decl_one [<<(RECDECL (RECCLAUSE $id (FUNVAR ($LIST $lvar))
-                     $body))>>] ->
-    [ $id [1 0 ] (FUNVAR ($LIST $lvar)) [1 0] "->" [1 0] $body:E ]
-  ;
-
-(* ============================== *)
-(*     PP rules for tacticals     *)
-(* ============================== *)
-
-  level 0:
-  | idtac  [<<(IDTAC)>>]            -> ["Idtac"]
-  | fail   [<<(FAIL)>>]             -> ["Fail"]
-  | 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] "]"]
-  | abstract_anon [<<(ABSTRACT (TACTIC $t))>>] -> ["Abstract " $t:E]
-  | abstract_name [<<(ABSTRACT ($VAR $id) (TACTIC $t))>>] ->
-    ["Abstract " $t:E " using "  $id]
-  | eval  [<<(EVAL $c (REDEXP $rtc))>>] ->
-    ["Eval" [1 0] (REDEXP $rtc) [1 0] "in" [1 0] (COMMAND $c)]
-  | inst  [<<(CONTEXT $id $c)>>] -> ["Inst" [1 0] $id "[" (COMMAND $c) "]"]
-  | check [<<(CHECK $c)>>] -> ["Check" [1 0] (COMMAND $c)]
-
-(* =================================== *)
-(*     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))] ]
-  | clear_body [<<(ClearBody (CLAUSE ($LIST $l)))>>] ->
-          [ [<hov 3> "ClearBody " (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]
-  | newinductionid [<<(NewInduction $id)>>] -> ["NewInduction " $id]
-  | newinductionnum [<<(NewInduction ($NUM $n))>>] -> ["NewInduction " $n]
-
-  | destructid [<<(Destruct $id)>>] -> ["Destruct " $id]
-  | destructnum [<<(Destruct ($NUM $n))>>] -> ["Destruct " $n]
-  | newdestructid [<<(NewDestruct $id)>>] -> ["NewDestruct " $id]
-  | newdestructnum [<<(NewDestruct ($NUM $n))>>] -> ["NewDestruct " $n]
-
-  | decomposeand [<<(DecomposeAnd $c)>>] -> [ "Decompose Record " $c ]
-  | decomposeor [<<(DecomposeOr $c)>>] -> [ "Decompose Sum " $c ]
-  | decomposethese [<<(DecomposeThese $c ($LIST $l))>>] -> 
-              ["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]
-  | truecutid [<<(TrueCut $C $id)>>] -> ["Assert " $id " : " $C]
-  | truecut [<<(TrueCut $C)>>] -> ["Assert " $C]
-  | forward [<<(Forward _ $C $id)>>] -> ["Assert " $id " := " $C]
-  | pose_named [<<(Forward "KeepBody" $C $id)>>] -> ["Pose " $id " := " $C]
-  | pose_anon  [<<(Forward "KeepBody" $C)>>] -> ["Pose " $C]
-
-  | lettac_cons [<<(LetTac $id $c (LETPATTERNS $p ($LIST $pl)))>>] -> 
-	["LetTac" [1 1] $id ":=" $c [1 1] "in" [1 1] (LETPATTERNS $p ($LIST $pl))]
-  | lettac_nil [<<(LetTac $id $c (LETPATTERNS))>>] -> 
-	["LetTac" [1 1] $id ":=" $c]
-
-  | 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]
-
-(* ===================================== *)
-(*     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) (Zeta)))>>] ->
-       [ "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))]
-  | flags_zeta [<<(FLAGS (Zeta) ($LIST $F))>>] ->
-        [ [1 0] "Zeta" (FLAGS ($LIST $F))]
-  | delta_unf [<<(FLAGS (Unf ($LIST $idl)) ($LIST $F))>>]
-         -> [ [1 0] "[" [<hov 0> (LISTSPC ($LIST $idl)) ] "]"
-              (FLAGS ($LIST $F))]
-  | delta_unfbut [<<(FLAGS (UnfBut ($LIST $idl)) ($LIST $F))>>]
-         -> [ [1 0] "-[" [<hov 0> (LISTSPC ($LIST $idl)) ] "]"
-              (FLAGS ($LIST $F))]
-  | 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 ]
-  | intropatwild [<<(WILDCAR)>>] -> [ "_" ]
-
-
-  | 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)>>] -> [ ]
-
-
-  (* Hypotheses *)
-  | inhyp [<<(INHYP $x)>>] -> [ $x ]
-  | inhyptype [<<(INHYPTYPE $x)>>] -> [ "(Type of " $x ")" ]
-
-  (* 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 )>>] -> [ ]
-
-  (* Only when debugging *)
-  | prim_tactic [<<(PRIMTACTIC $tac)>>] -> [ $tac ]
-  ;
-
-  level 8:
-    tactic_to_constr [<<(COMMAND $c)>>] -> [ $c:"constr":9 ]
-  | tactic_to_castedconstr [<<(CASTEDCOMMAND $c)>>] -> [ $c:"constr":9 ]
-  | tactic_to_openconstr [<<(CASTEDOPENCOMMAND $c)>>] -> [ $c:"constr":9 ]
-
-  (* Some operations over constr to be pretty-printed here *)
-  | eval_command  [<<(COMMAND (EVAL $c (REDEXP $rtc)))>>] ->
-    [(EVAL $c (REDEXP $rtc))]
-  | inst_command  [<<(COMMAND (CONTEXT $id $c))>>] -> [(CONTEXT $id $c)]
-  | check_command [<<(COMMAND (CHECK $c))>>] -> [(CHECK $c)]
-
-  (* This is produced bu UNFOLDLIST *)
-  | tactic_qualidarg_constr [<<(COMMAND (QUALIDARG $p))>>] -> [(QUALIDARG $p)]
-  | tactic_qualidarg_nil [<<(QUALIDARG $id)>>] -> [ $id ]
-  | tactic_qualidarg_cons [<<(QUALIDARG $id $p)>>] ->
-	 [ $id [1 0] "." (QUALID $p) ].