diff options
author | 2017-06-29 16:32:05 +0200 | |
---|---|---|
committer | 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 7d0728458..4e8b98fcf 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: |