Changement du parseur par défaut dans Syntax

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

1 files changed, 7 insertions, 6 deletions

diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v
index 5bf2cedaa..06a9c123d 100644
--- a/theories/Wellfounded/Lexicographic_Exponentiation.v
+++ b/theories/Wellfounded/Lexicographic_Exponentiation.v
@@ -30,17 +30,18 @@ Syntactic Definition Cons := (cons 1!A).
 
 Syntax constr
   level 1:
-    List [<<(list A)>>] -> ["List"]
-  | Nil  [<<(nil A)>>] -> ["Nil"]
-  | Cons [<<(cons A)>>] -> ["Cons"]
+    List [ (list A) ] -> ["List"]
+  | Nil  [ (nil A) ] -> ["Nil"]
+  | Cons [ (cons A) ] -> ["Cons"]
   ;
   level 10:
-    Cons2 [<<(cons A $e $l)>>] -> ["Cons " $e:L " " $l:L ].
+    Cons2 [ (cons A $e $l) ] -> ["Cons " $e:L " " $l:L ].
 
 Hints Resolve d_one d_nil  t_step.
 
-Syntax constr level 1:
-  pair_sig [<<(exist (list A) Desc $e $d)>>] -> ["<<" $e:L "," $d:L ">>"].
+Syntax constr
+  level 1:
+  pair_sig [ (exist (list A) Desc $e $d) ] -> ["<<" $e:L "," $d:L ">>"].
 
 
 Lemma left_prefix : (x,y,z:List)(ltl x^y z)-> (ltl x z).