diff options
| author |  mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-07-13 16:16:56 +0000 |
|---|---|---|
| committer | mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-07-13 16:16:56 +0000 |
| commit | e58c719dc424dd8fd734b8fed182670cbe37d3c8 (patch) | |
| tree | 672c3b497a40a9063579e60a69bcba6d2a9470a0 /parsing/g_vernac.ml4 | |
| parent | 59300a9da64103024e8dd90b89b5528729d20a3e (diff) | |
reparation regles pour parsing Coercion Local
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1849 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index e4edb1fad..20bc8732d 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) >> |