diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.ml4 | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 499e7b0531..81645a580f 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -152,7 +152,9 @@ GEXTEND Gram sort: [ [ "Set" -> GSet | "Prop" -> GProp - | "Type" -> GType None ] ] + | "Type" -> GType None + | "Type"; "{"; id = string; "}" -> GType (Some id) + ] ] ; lconstr: [ [ c = operconstr LEVEL "200" -> c ] ] @@ -277,13 +279,17 @@ GEXTEND Gram | c=operconstr LEVEL "9" -> (c,None) ] ] ; atomic_constr: - [ [ g=global -> CRef (g,None) + [ [ g=global; i=instance -> CRef (g,i) | s=sort -> CSort (!@loc,s) | 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)) ] ] ; + instance: + [ [ "@{"; l = LIST1 sort SEP ","; "}" -> Some l + | -> None ] ] + ; fix_constr: [ [ fx1=single_fix -> mk_single_fix fx1 | (_,kw,dcl1)=single_fix; "with"; dcls=LIST1 fix_decl SEP "with"; |