diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-11 20:00:27 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-12 10:39:32 +0200 |
| commit | ca300977724a6b065a98c025d400c71f41b9df4b (patch) | |
| tree | 59a2fd3327b3d0eb9cd1e11cbb31605f2a08ea27 /parsing | |
| parent | 012fe1a96ba81ab0a7fa210610e3f25187baaf1d (diff) | |
Parsing evar instances.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.ml4 | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 272a18c3e..18012f8a1 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -193,7 +193,7 @@ GEXTEND Gram | "@"; f=global; i = instance; args=LIST0 NEXT -> CAppExpl(!@loc,(None,f,i),args) | "@"; (locid,id) = pattern_identref; args=LIST1 identref -> let args = List.map (fun x -> CRef (Ident x,None), None) args in - CApp(!@loc,(None,CPatVar(locid,(true,id))),args) ] + CApp(!@loc,(None,CPatVar(locid,id)),args) ] | "9" [ ".."; c = operconstr LEVEL "0"; ".." -> CAppExpl (!@loc,(None,Ident (!@loc,ldots_var),None),[c]) ] @@ -289,7 +289,14 @@ GEXTEND Gram | n=INT -> CPrim (!@loc, Numeral (Bigint.of_string n)) | s=string -> CPrim (!@loc, String s) | "_" -> CHole (!@loc, None, None) - | id=pattern_ident -> CPatVar(!@loc,(false,id)) ] ] + | id=pattern_ident; inst = evar_instance -> CEvar(!@loc,id,inst) ] ] + ; + inst: + [ [ id = ident; ":="; c = lconstr -> (id,c) ] ] + ; + evar_instance: + [ [ "@{"; l = LIST1 inst SEP ","; "}" -> l + | -> [] ] ] ; instance: [ [ "@{"; l = LIST1 level; "}" -> Some l |