diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-01-24 16:19:49 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-01-24 16:19:49 +0000 |
| commit | 49d89ef0a7d3baaa28d76e66ce4658d8cc6155b6 (patch) | |
| tree | 63d9a9951ba4786562cecd4722a00306d4ad99cd /parsing | |
| parent | fd07bda1ac92972c4224868f6d9dfeb430b7f379 (diff) | |
Ajout de constantes locales dans les Records
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1266 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 7f22ba49a..c628c2baf 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -230,10 +230,12 @@ GEXTEND Gram ; field: [ [ id = identarg; oc = of_type_with_opt_coercion; c = constrarg -> - <:ast< (VERNACARGLIST ($STR $oc) $id $c) >> - | id = identarg; ":="; b = constrarg; - oc = of_type_with_opt_coercion; c = constrarg -> - <:ast< (VERNACARGLIST ($STR $oc) $id $c $b) >> + <:ast< (VERNACARGLIST ($STR $oc) "ASSUM" $id $c) >> + | id = identarg; oc = of_type_with_opt_coercion; t = Constr.constr; + ":="; b = Constr.constr -> + <:ast< (VERNACARGLIST "" "DEF" $id $b (COMMAND (CAST $b $t))) >> + | id = identarg; ":="; b = constrarg -> + <:ast< (VERNACARGLIST "" "DEF" $id $b) >> (* | id = identarg; ":>"; c = constrarg -> <:ast< (VERNACARGLIST "COERCION" $id $c) >> *)] ] ; |