diff options
| -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: |