diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-09-27 06:38:34 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-09-27 06:38:34 +0000 |
| commit | 8400196955b62022e5fd0a747dde0232ec9ed1ab (patch) | |
| tree | efee3998567961a24db4888f72c76ebe172b9b63 /parsing | |
| parent | 8d5da894b55943f59ebdb98c22432933939568a8 (diff) | |
report d'une correction de Bruno
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@80 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_command.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/g_command.ml4 b/parsing/g_command.ml4 index 98b2d16e4..f820ef44b 100644 --- a/parsing/g_command.ml4 +++ b/parsing/g_command.ml4 @@ -26,7 +26,7 @@ GEXTEND Gram [ [ "?" -> <:ast< (XTRA "ISEVAR") >> | "?"; n = Prim.number -> <:ast< (META $n) >> | "["; id1 = IDENT; ":"; c = command; c2 = abstraction_tail -> - <:ast< (LAMBDA $c [$id1]$c2) >> + <:ast< (LAMBDALIST $c [$id1]$c2) >> | "["; id1 = IDENT; ","; idl = ne_ident_comma_list; ":"; c = command; c2 = abstraction_tail -> <:ast< (LAMBDALIST $c [$id1]($SLAM $idl $c2)) >> @@ -34,7 +34,7 @@ GEXTEND Gram c = abstraction_tail -> <:ast< (LAMBDALIST (XTRA "ISEVAR") [$id1]($SLAM $idl $c)) >> | "["; id1 = IDENT; c = abstraction_tail -> - <:ast< (LAMBDA (XTRA "ISEVAR") [$id1]$c) >> + <:ast< (LAMBDALIST (XTRA "ISEVAR") [$id1]$c) >> | "["; id1 = IDENT; "="; c = command; "]"; c2 = command -> <:ast< (ABST #Core#let.cci $c [$id1]$c2) >> | "<<"; id1 = IDENT; ">>"; c = command -> <:ast< [$id1]$c >> |