diff options
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 69ba73c673..86fa5518cc 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -153,7 +153,7 @@ GEXTEND Gram [ [ "Set" -> GSet | "Prop" -> GProp | "Type" -> GType None - | "Type"; "{"; id = string; "}" -> GType (Some id) + | "Type"; "{"; id = ident; "}" -> GType (Some (Id.to_string id)) ] ] ; lconstr: @@ -287,9 +287,16 @@ GEXTEND Gram | id=pattern_ident -> CPatVar(!@loc,(false,id)) ] ] ; instance: - [ [ "@{"; l = LIST1 sort SEP ","; "}" -> Some l + [ [ "@{"; l = LIST1 level; "}" -> Some l | -> None ] ] ; + level: + [ [ "Set" -> GSet + | "Prop" -> GProp + | "Type" -> GType None + | id = ident -> GType (Some (Id.to_string id)) + ] ] + ; fix_constr: [ [ fx1=single_fix -> mk_single_fix fx1 | (_,kw,dcl1)=single_fix; "with"; dcls=LIST1 fix_decl SEP "with"; |