Changement parser par défaut dans Syntax

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

3 files changed, 60 insertions, 60 deletions

diff --git a/tactics/EAuto.v b/tactics/EAuto.v
index f56d9aadc1..5c1994c5b1 100644
--- a/tactics/EAuto.v
+++ b/tactics/EAuto.v
@@ -35,30 +35,30 @@ Grammar tactic simple_tactic: Ast :=
 	-> [(EAuto $n "*")].
 
 Syntax tactic level 0:
-  eauto_with [(EAuto ($LIST $lid))] -> 
+  eauto_with [<<(EAuto ($LIST $lid))>>] -> 
 	[ "EAuto" [1 0] "with " [<hov 0> (LISTSPC ($LIST $lid))] ]
-| eauto [(EAuto)] -> ["EAuto"]
-| eauto_n_with [(EAuto ($NUM $n) ($LIST $lid))] ->
+| eauto [<<(EAuto)>>] -> ["EAuto"]
+| eauto_n_with [<<(EAuto ($NUM $n) ($LIST $lid))>>] ->
 	[ "EAuto " $n [1 0] "with " [<hov 0> (LISTSPC ($LIST $lid))] ]
-| eauto_n [(EAuto ($NUM $n))] -> ["EAuto " $n]
-| eauto_with_star [(EAuto "*")] -> 
+| eauto_n [<<(EAuto ($NUM $n))>>] -> ["EAuto " $n]
+| eauto_with_star [<<(EAuto "*")>>] -> 
 	[ "EAuto with *" ]
-| eauto_n_with_star [(EAuto ($NUM $n) "*")] ->
+| eauto_n_with_star [<<(EAuto ($NUM $n) "*")>>] ->
 	[ "EAuto " $n " with *" ]
-| etrivial [(ETrivial)] -> ["ETrivial"]
+| etrivial [<<(ETrivial)>>] -> ["ETrivial"]
 
-| eexact [(EExact $c)] -> ["EExact " $c]
+| eexact [<<(EExact $c)>>] -> ["EExact " $c]
 
-| eapply [(EApplyWithBindings $c ($LIST $bl))]
+| eapply [<<(EApplyWithBindings $c ($LIST $bl))>>]
       -> ["EApply " $c (WITHBINDING ($LIST $bl))]
 
-| prolog [(Prolog ($NUM $n) ($LIST $l))]
+| prolog [<<(Prolog ($NUM $n) ($LIST $l))>>]
     -> [ [<hov 0> "Prolog" [1 2] "[" [<hov 0> (LISTSPC ($LIST $l)) ] "]"
                   [1 2] $n] ]
 
-| instantiate [(Instantiate ($NUM $n) $c)] -> ["Instantiate " $n [1 2] $c]
+| instantiate [<<(Instantiate ($NUM $n) $c)>>] -> ["Instantiate " $n [1 2] $c]
 
-| normevars [(NormEvars)] -> ["NormEvars"].
+| normevars [<<(NormEvars)>>] -> ["NormEvars"].
 
 
 (* $Id$ *)
diff --git a/tactics/Equality.v b/tactics/Equality.v
index 95739e8388..66193ca212 100644
--- a/tactics/Equality.v
+++ b/tactics/Equality.v
@@ -120,59 +120,59 @@ Grammar tactic simple_tactic: Ast :=
       -> [(SubstHyp_RL $eqn $id)].
 
 Syntax tactic level 0:
-  replace [(Replace $c1 $c2)] -> ["Replace " $c1 [1 1] "with " $c2]
+  replace [<<(Replace $c1 $c2)>>] -> ["Replace " $c1 [1 1] "with " $c2]
 
-| deqhyp [(DEqHyp $id)] -> ["Simplify_eq " $id]
-| deqconcl [(DEqConcl)] -> ["Simplify_eq"]
+| deqhyp [<<(DEqHyp $id)>>] -> ["Simplify_eq " $id]
+| deqconcl [<<(DEqConcl)>>] -> ["Simplify_eq"]
 
-| discr_id [(DiscrHyp $id)] -> ["Discriminate " $id]
-| discr [(Discr)] -> ["Discriminate"]
+| discr_id [<<(DiscrHyp $id)>>] -> ["Discriminate " $id]
+| discr [<<(Discr)>>] -> ["Discriminate"]
 
-| inj [(Inj)] -> ["Injection"]
-| inj_id [(InjHyp $id)] -> ["Injection " $id]
+| inj [<<(Inj)>>] -> ["Injection"]
+| inj_id [<<(InjHyp $id)>>] -> ["Injection " $id]
 
-| rewritelr [(RewriteLR $C ($LIST $bl))] -> ["Rewrite " $C (WITHBINDING ($LIST $bl))]
-| rewriterl [(RewriteRL $C ($LIST $bl))] -> ["Rewrite <- " $C (WITHBINDING ($LIST $bl))]
+| rewritelr [<<(RewriteLR $C ($LIST $bl))>>] -> ["Rewrite " $C (WITHBINDING ($LIST $bl))]
+| rewriterl [<<(RewriteRL $C ($LIST $bl))>>] -> ["Rewrite <- " $C (WITHBINDING ($LIST $bl))]
 
-| condrewritelr [(CondRewriteLR (TACTIC $tac) $C ($LIST $bl))] -> ["Conditional " $tac [1 1] "Rewrite " $C (WITHBINDING ($LIST $bl))]
-| condrewriterl [(CondRewriteRL (TACTIC $tac) $C ($LIST $bl))] -> ["Conditional "  $tac [1 1] "Rewrite <- " $C (WITHBINDING ($LIST $bl))]
+| condrewritelr [<<(CondRewriteLR (TACTIC $tac) $C ($LIST $bl))>>] -> ["Conditional " $tac [1 1] "Rewrite " $C (WITHBINDING ($LIST $bl))]
+| condrewriterl [<<(CondRewriteRL (TACTIC $tac) $C ($LIST $bl))>>] -> ["Conditional "  $tac [1 1] "Rewrite <- " $C (WITHBINDING ($LIST $bl))]
 
-| rewriteLR_in [(RewriteLRin $h $c ($LIST $bl))] -> ["Rewrite " $c (WITHBINDING ($LIST $bl)) [1 1] "in " $h]
-| rewriteRL_in [(RewriteRLin $h $c ($LIST $bl))] -> ["Rewrite <- " $c (WITHBINDING ($LIST $bl)) [1 1]"in " $h]
+| rewriteLR_in [<<(RewriteLRin $h $c ($LIST $bl))>>] -> ["Rewrite " $c (WITHBINDING ($LIST $bl)) [1 1] "in " $h]
+| rewriteRL_in [<<(RewriteRLin $h $c ($LIST $bl))>>] -> ["Rewrite <- " $c (WITHBINDING ($LIST $bl)) [1 1]"in " $h]
 
-| condrewritelrin [(CondRewriteLRin (TACTIC $tac) $h $C ($LIST $bl))] -> ["Conditional " $tac [1 1] "Rewrite " $C (WITHBINDING ($LIST $bl)) [1 1] "in " $h]
-| condrewriterlin [(CondRewriteRLin (TACTIC $tac) $h $C ($LIST $bl))] -> ["Conditional "  $tac [1 1] "Rewrite <- " $C (WITHBINDING ($LIST $bl)) [1 1] "in " $h]
+| condrewritelrin [<<(CondRewriteLRin (TACTIC $tac) $h $C ($LIST $bl))>>] -> ["Conditional " $tac [1 1] "Rewrite " $C (WITHBINDING ($LIST $bl)) [1 1] "in " $h]
+| condrewriterlin [<<(CondRewriteRLin (TACTIC $tac) $h $C ($LIST $bl))>>] -> ["Conditional "  $tac [1 1] "Rewrite <- " $C (WITHBINDING ($LIST $bl)) [1 1] "in " $h]
 
 
-| DRewriteLR [(SubstHypInConcl_LR $id)] -> ["Dependent Rewrite -> " $id]
-| DRewriteRL [(SubstHypInConcl_RL $id)] -> ["Dependent Rewrite <- " $id]
+| DRewriteLR [<<(SubstHypInConcl_LR $id)>>] -> ["Dependent Rewrite -> " $id]
+| DRewriteRL [<<(SubstHypInConcl_RL $id)>>] -> ["Dependent Rewrite <- " $id]
 
-| cutrewriteLR [(SubstConcl_LR $eqn)] -> ["CutRewrite -> " $eqn]
-| cutrewriteLRin [(SubstHyp_LR $eqn $id)]
+| cutrewriteLR [<<(SubstConcl_LR $eqn)>>] -> ["CutRewrite -> " $eqn]
+| cutrewriteLRin [<<(SubstHyp_LR $eqn $id)>>]
      -> ["CutRewrite -> " $eqn:E [1 1]"in " $id]
 
-| cutrewriteRL [(SubstConcl_RL $eqn)] -> ["CutRewrite <- " $eqn:E]
-| cutrewriteRLin [(SubstHyp_RL $eqn $id)]
+| cutrewriteRL [<<(SubstConcl_RL $eqn)>>] -> ["CutRewrite <- " $eqn:E]
+| cutrewriteRLin [<<(SubstHyp_RL $eqn $id)>>]
       -> ["CutRewrite <- " $eqn:E [1 1]"in " $id]
-|nil_consbase [(CONSBASE)] -> []
-|single_consbase [(CONSBASE $tac)] -> [[1 0] $tac]
-|nil_ortactic [(ORTACTIC)] -> []
-|single_ortactic [(ORTACTIC $tac)] -> ["|" $tac]
-|AutoRewrite [(AutoRewrite $id)] -> ["AutoRewrite " $id]
-|AutoRewriteBaseList [(REDEXP (BaseList $ft ($LIST $tl)))] ->
+|nil_consbase [<<(CONSBASE)>>] -> []
+|single_consbase [<<(CONSBASE $tac)>>] -> [[1 0] $tac]
+|nil_ortactic [<<(ORTACTIC)>>] -> []
+|single_ortactic [<<(ORTACTIC $tac)>>] -> ["|" $tac]
+|AutoRewrite [<<(AutoRewrite $id)>>] -> ["AutoRewrite " $id]
+|AutoRewriteBaseList [<<(REDEXP (BaseList $ft ($LIST $tl)))>>] ->
   ["[" $ft (CONSBASE ($LIST $tl)) "]"]
-|AutoRewriteStep [(REDEXP (Step $ft ($LIST $tl)))] ->
+|AutoRewriteStep [<<(REDEXP (Step $ft ($LIST $tl)))>>] ->
   [[0 1] "Step=" "[" $ft (ORTACTIC ($LIST $tl)) "]"]
-|AutoRewriteRest [(REDEXP (Rest $ft ($LIST $tl)))] ->
+|AutoRewriteRest [<<(REDEXP (Rest $ft ($LIST $tl)))>>] ->
   [[0 1] "Rest=" "[" $ft (ORTACTIC ($LIST $tl)) "]"]
-|AutoRewriteSolveStep [(REDEXP (SolveStep))] -> ["with Solve"]
-|AutoRewriteSolveRest [(REDEXP (SolveRest))] -> ["with Solve"]
-|AutoRewriteUse [(REDEXP (Use))] -> ["with Use"]
-|AutoRewriteAll [(REDEXP (All))] -> ["with All"]
-|AutoRewriteCond [(REDEXP (Cond))] -> ["with Cond"]
-|AutoRewriteDepth [(REDEXP (Depth $dth))] -> [[0 1] "Depth=" $dth]
-|AutoRewriteByName [(REDEXP (ByName $id))] -> [ $id ]
-|AutoRewriteExplicit [(REDEXP (Explicit $l))] -> ["[" $l "]"]
-|AutoRewriteLR [(REDEXP (LR $c))] -> [ $c "LR" ]
-|AutoRewriteRL [(REDEXP (RL $c))] -> [ $c "RL" ]
+|AutoRewriteSolveStep [<<(REDEXP (SolveStep))>>] -> ["with Solve"]
+|AutoRewriteSolveRest [<<(REDEXP (SolveRest))>>] -> ["with Solve"]
+|AutoRewriteUse [<<(REDEXP (Use))>>] -> ["with Use"]
+|AutoRewriteAll [<<(REDEXP (All))>>] -> ["with All"]
+|AutoRewriteCond [<<(REDEXP (Cond))>>] -> ["with Cond"]
+|AutoRewriteDepth [<<(REDEXP (Depth $dth))>>] -> [[0 1] "Depth=" $dth]
+|AutoRewriteByName [<<(REDEXP (ByName $id))>>] -> [ $id ]
+|AutoRewriteExplicit [<<(REDEXP (Explicit $l))>>] -> ["[" $l "]"]
+|AutoRewriteLR [<<(REDEXP (LR $c))>>] -> [ $c "LR" ]
+|AutoRewriteRL [<<(REDEXP (RL $c))>>] -> [ $c "RL" ]
 .
diff --git a/tactics/Inv.v b/tactics/Inv.v
index d2df140e5f..2bde23bf72 100644
--- a/tactics/Inv.v
+++ b/tactics/Inv.v
@@ -6,24 +6,24 @@ Require Export Equality.
 Declare ML Module "Inv" "Leminv".
 
 Syntax tactic level 0:
-  inversion    [(Inv $ic $id)] -> [ (INVCOM $ic) [1 1] $id]
-| inversion_in [(InvIn $ic $id ($LIST $l))]
+  inversion    [<<(Inv $ic $id)>>] -> [ (INVCOM $ic) [1 1] $id]
+| inversion_in [<<(InvIn $ic $id ($LIST $l))>>]
     -> [ (INVCOM $ic) [1 1] $id (CLAUSE ($LIST $l))]
 
-| dep_inv [(DInv $ic $id)] -> ["Dependent " (INVCOM $ic) [1 1] $id]
-| dep_inv_with [(DInvWith $ic $id $c)]
+| dep_inv [<<(DInv $ic $id)>>] -> ["Dependent " (INVCOM $ic) [1 1] $id]
+| dep_inv_with [<<(DInvWith $ic $id $c)>>]
     -> ["Dependent " (INVCOM $ic) [1 1] $id [1 1] "with " $c]
 
 (* Use rules *)
 
 | inv_using
-    [(UseInversionLemma $id $c)] -> ["Inversion " $id [1 1] "using " $c]
-| inv_using_in [(UseInversionLemmaIn $id $c ($LIST $l))]
+    [<<(UseInversionLemma $id $c)>>] -> ["Inversion " $id [1 1] "using " $c]
+| inv_using_in [<<(UseInversionLemmaIn $id $c ($LIST $l))>>]
     -> ["Inversion " $id [1 1] "using " $c (CLAUSE ($LIST $l))]
 
-| simple_inv       [(INVCOM HalfInversion)] -> [ "Simple Inversion" ]
-| inversion_com    [(INVCOM Inversion)] -> [ "Inversion" ]
-| inversion_clear  [(INVCOM InversionClear)] -> [ "Inversion_clear" ].
+| simple_inv       [<<(INVCOM HalfInversion)>>] -> [ "Simple Inversion" ]
+| inversion_com    [<<(INVCOM Inversion)>>] -> [ "Inversion" ]
+| inversion_clear  [<<(INVCOM InversionClear)>>] -> [ "Inversion_clear" ].
 
 
 Grammar tactic simple_tactic: Ast :=