X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_textual_parser%2FcicTextualParser.mly;h=5afd56ed9d75e29110c85f12a496b8148e4e8fae;hb=fb12bdf2cf0ecbf50726b70d6a3097cb933319a0;hp=11313aeff68743f0a9df2048ec34d2c93f8d306f;hpb=29c5eaa7408d2e35805817d50c4e0bc93f100e1e;p=helm.git diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly index 11313aeff..5afd56ed9 100644 --- a/helm/ocaml/cic_textual_parser/cicTextualParser.mly +++ b/helm/ocaml/cic_textual_parser/cicTextualParser.mly @@ -297,14 +297,16 @@ expr2: { let dom,mk_substitutionlist = $3 in dom, function interp -> Meta ($1, mk_substitutionlist interp) } - | LPAREN expr expr exprlist RPAREN - { let dom1,mk_expr1 = $2 in - let dom2,mk_expr2 = $3 in - let dom3,mk_exprlist = $4 in - let dom = union dom1 (union dom2 dom3) in - dom, - function interp -> - Appl ([mk_expr1 interp ; mk_expr2 interp]@(mk_exprlist interp)) + | LPAREN expr exprlist RPAREN + { let length,dom2,mk_exprlist = $3 in + match length with + 0 -> $2 + | _ -> + let dom1,mk_expr1 = $2 in + let dom = union dom1 dom2 in + dom, + function interp -> + Appl ((mk_expr1 interp)::(mk_exprlist interp)) } ; exp_named_subst : @@ -417,11 +419,6 @@ pihead: let dom,mk_expr = $1 in Anonymous, (dom, function interp -> mk_expr interp) } - | LPAREN expr RPAREN ARROW - { CicTextualParser0.binders := (Some Anonymous)::!CicTextualParser0.binders ; - let dom,mk_expr = $2 in - Anonymous, (dom, function interp -> mk_expr interp) - } | PROD ID DOT { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders; let newmeta = new_meta () in @@ -478,12 +475,12 @@ branches: ; exprlist: - { [], function _ -> [] } + { 0, [], function _ -> [] } | expr exprlist { let dom1,mk_expr = $1 in - let dom2,mk_exprlist = $2 in + let length,dom2,mk_exprlist = $2 in let dom = union dom1 dom2 in - dom, function interp -> (mk_expr interp)::(mk_exprlist interp) + length+1, dom, function interp -> (mk_expr interp)::(mk_exprlist interp) } ; exprseplist: