From 96346162116fda030b177a0816d665f7493b0ef4 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 2 Jun 2000 12:35:33 +0000
Subject: ':>' est devenu un seul token

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@486 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_vernac.ml4 | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index bea4c46aa5..f29f4407e0 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -178,6 +178,11 @@ GEXTEND Gram
     [ [ ">" -> "COERCION"
       |  -> "" ] ]
   ;
+  of_type_with_opt_coercion:
+    [ [ ":>" -> "COERCION"
+      | ":"; ">" -> "COERCION"
+      | ":" -> "" ] ]
+  ;
   onescheme:
     [ [ id = identarg; ":="; dep = dep; indid = identarg; IDENT "Sort";
         s = sortarg ->
@@ -209,7 +214,7 @@ GEXTEND Gram
       | corec = onecorec -> [corec] ] ]
   ;
   field:
-    [ [ id = identarg; ":"; oc = opt_coercion; c = constrarg ->
+    [ [ id = identarg; oc = of_type_with_opt_coercion; c = constrarg ->
           <:ast< (VERNACARGLIST ($STR $oc) $id $c) >>
 (*      | id = identarg; ":>"; c = constrarg ->
           <:ast< (VERNACARGLIST "COERCION" $id $c) >> *)] ]
-- 
cgit v1.2.3