From e58c719dc424dd8fd734b8fed182670cbe37d3c8 Mon Sep 17 00:00:00 2001
From: mohring
Date: Fri, 13 Jul 2001 16:16:56 +0000
Subject: reparation regles pour parsing Coercion Local

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1849 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_vernac.ml4 | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index e4edb1fad2..20bc8732d4 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -348,23 +348,25 @@ GEXTEND Gram
       | IDENT "Coercion"; qid = qualidarg; ":="; c = def_body ->
           let s = Ast.coerce_to_var "qid" qid in
           <:ast< (DEFINITION "COERCION" ($VAR $s) $c) >>
-      | IDENT "Coercion"; IDENT "Local"; s = identarg; ":="; 
+      | IDENT "Coercion"; IDENT "Local"; qid = qualidarg; ":="; 
 	 c = constrarg ->
-          <:ast< (DEFINITION "LCOERCION" $s $c) >>
-      | IDENT "Coercion"; IDENT "Local"; s = identarg; ":="; 
+          let s = Ast.coerce_to_var "qid" qid in
+	    <:ast< (DEFINITION "LCOERCION" ($VAR $s) $c) >>
+      | IDENT "Coercion"; IDENT "Local"; qid = qualidarg; ":="; 
 	 c1 = Constr.constr; ":"; c2 = Constr.constr ->
-          <:ast< (DEFINITION "LCOERCION" $s (CONSTR (CAST $c1 $c2))) >>
+          let s = Ast.coerce_to_var "qid" qid in
+          <:ast< (DEFINITION "LCOERCION" ($VAR $s) (CONSTR (CAST $c1 $c2))) >>
       | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = qualidarg;
          ":"; c = qualidarg; ">->"; d = qualidarg ->
           <:ast< (COERCION "LOCAL" "IDENTITY" $f $c $d) >>
       | IDENT "Identity"; IDENT "Coercion"; f = qualidarg; ":";
          c = qualidarg; ">->"; d = qualidarg ->
           <:ast< (COERCION "" "IDENTITY" $f $c $d) >>
-      | IDENT "Coercion"; IDENT "Local"; f = qualidarg; ":"; c = qualidarg;
+      | IDENT "Coercion"; IDENT "Local"; qid = qualidarg; ":"; c = qualidarg;
         ">->"; d = qualidarg ->
-          <:ast< (COERCION "LOCAL" "" $f $c $d) >>
-      | IDENT "Coercion"; f = qualidarg; ":"; c = qualidarg; ">->";
-         d = qualidarg -> <:ast< (COERCION "" "" $f $c $d) >>
+          <:ast< (COERCION "LOCAL" "" $qid $c $d) >>
+      | IDENT "Coercion"; qid = qualidarg; ":"; c = qualidarg; ">->";
+         d = qualidarg -> <:ast< (COERCION "" "" $qid $c $d) >>
       | IDENT "Class"; IDENT "Local"; c = qualidarg ->
           <:ast< (CLASS "LOCAL" $c) >>
       | IDENT "Class"; c = qualidarg -> <:ast< (CLASS "" $c) >>
-- 
cgit v1.2.3