diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.ml4 | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index c2ce003f1..9f12db649 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -219,6 +219,8 @@ GEXTEND Gram CAst.make ~loc:(!@loc) @@ CNotation("( _ )",([c],[],[],[])) | _ -> c) | "{|"; c = record_declaration; "|}" -> c + | "{"; c = binder_constr ; "}" -> + CAst.make ~loc:(!@loc) @@ CNotation(("{ _ }"),([c],[],[],[])) | "`{"; c = operconstr LEVEL "200"; "}" -> CAst.make ~loc:(!@loc) @@ CGeneralization (Implicit, None, c) | "`("; c = operconstr LEVEL "200"; ")" -> |