diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-08 14:05:24 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-08 14:05:24 +0000 |
| commit | 8640627fa00798b429baf56937a66f1621be0a02 (patch) | |
| tree | c944bab5d696874e1eca84b92334430c6329fd9f | |
| parent | afe0053676782fa7c990af622e95924d6ce5aaf7 (diff) | |
Prise en compte de la syntaxe [x:=c:t]b comme équivalent de [x:=c::t]b
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2170 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/g_constr.ml4 | 16 | ||||
| -rwxr-xr-x | syntax/PPConstr.v | 3 |
2 files changed, 11 insertions, 8 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 92e2262f3..ca5f582d9 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -124,13 +124,9 @@ GEXTEND Gram c = constr; "in"; c1 = constr -> <:ast< (LET "SYNTH" $c ($ABSTRACT "LAMBDALIST" (BINDERS (BINDER (ISEVAR) ($LIST $b))) $c1)) >> - | IDENT "let"; id1 = ident ; "="; c = constr; "in"; c1 = constr -> + | IDENT "let"; id1 = ident ; "="; c = opt_casted_constr; + "in"; c1 = constr -> <:ast< (LETIN $c [$id1]$c1) >> -(* - | IDENT "let"; id1 = IDENT ; "="; c = constr; "in"; c1 = constr -> - let id1 = Names.id_of_string id1 in - <:ast< (LETIN $c [$id1]$c1) >> -*) | IDENT "if"; c1 = constr; IDENT "then"; c2 = constr; IDENT "else"; c3 = constr -> <:ast< ( IF "SYNTH" $c1 $c2 $c3) >> @@ -188,12 +184,16 @@ GEXTEND Gram [ [ ","; idl = ne_ident_comma_list -> idl | -> [] ] ] ; + opt_casted_constr: + [ [ c = constr; ":"; t = constr -> <:ast< (CAST $c $t) >> + | c = constr -> c ] ] + ; vardecls: (* This is interpreted by Pcoq.abstract_binder *) [ [ id = ident; idl = ident_comma_list_tail; c = type_option -> <:ast< (BINDER $c $id ($LIST $idl)) >> - | id = ident; ":="; c = constr -> + | id = ident; ":="; c = opt_casted_constr -> <:ast< (LETIN $c $id) >> - | id = ident; "="; c = constr -> + | id = ident; "="; c = opt_casted_constr -> <:ast< (LETIN $c $id) >> ] ] ; ne_vardecls_list: diff --git a/syntax/PPConstr.v b/syntax/PPConstr.v index f78ef411e..ee259cbfa 100755 --- a/syntax/PPConstr.v +++ b/syntax/PPConstr.v @@ -144,8 +144,11 @@ Syntax constr [ $A:L [0 0] "->" (ARROWBOX $B) ] (* These are synonymous *) +(* redundant | let [ [$x = $M]$N ] -> [ [<hov 0> "[" $x "=" $M:E "]" [0 1] $N:E ] ] +*) | letin [ [$x := $A]$B ] -> [ [ <hov 0> "[" $x ":=" $A:E "]" [0 1] $B:E ] ] + | letincast [ [$x := $A : $C]$B ] -> [ [ <hov 0> "[" $x ":=" $A:E ":" $C:E "]" [0 1] $B:E ] ] ; (* Things parsed in command9 *) |