diff options
| author | Maxime Dénès | 2018-12-21 18:22:03 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-01-22 11:11:34 +0100 |
| commit | 3600f2cd55716550c4d9f78f05d43b6f33fd402e (patch) | |
| tree | 214e80f1d7e36db69a3d98ce610cc011d5940f91 | |
| parent | 4922d0d6e156338485b48ce3fd34c1179a505083 (diff) | |
Simplify parsing of instance binders
| -rw-r--r-- | vernac/g_vernac.mlg | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 0d3617b162..8ffdf74383 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -809,9 +809,8 @@ GRAMMAR EXTEND Gram | IDENT "transparent" -> { Conv_oracle.transparent } ] ] ; instance_name: - [ [ name = ident_decl; sup = OPT binders -> - { (CAst.map (fun id -> Name id) (fst name), snd name), - (Option.default [] sup) } + [ [ name = ident_decl; bl = binders -> + { (CAst.map (fun id -> Name id) (fst name), snd name), bl } | -> { ((CAst.make ~loc Anonymous), None), [] } ] ] ; hint_info: |