diff options
| author | Matthieu Sozeau | 2017-06-29 16:32:05 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2017-09-19 10:16:18 +0200 |
| commit | fc587e75d2d5d6e67365a9bc3a13ba5c86aba87b (patch) | |
| tree | 6938d979b36452db1f7092abda88a072c4ae7e01 | |
| parent | 296941dc97d53817cc58b4687ed99168e1dd33a9 (diff) | |
Allow empty instance parsing @{}
| -rw-r--r-- | parsing/g_constr.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 7d0728458b..4e8b98fcf2 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -301,7 +301,7 @@ GEXTEND Gram | -> [] ] ] ; instance: - [ [ "@{"; l = LIST1 universe_level; "}" -> Some l + [ [ "@{"; l = LIST0 universe_level; "}" -> Some l | -> None ] ] ; universe_level: |