diff options
Diffstat (limited to 'vernac/g_vernac.mlg')
| -rw-r--r-- | vernac/g_vernac.mlg | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index b5bc1c8111..0d3617b162 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -695,7 +695,7 @@ GRAMMAR EXTEND Gram let insts = List.map (fun i -> (i, info)) ids in VernacExistingInstance insts } - | IDENT "Existing"; IDENT "Class"; is = global -> { VernacDeclareClass is } + | IDENT "Existing"; IDENT "Class"; is = global -> { VernacExistingClass is } (* Arguments *) | IDENT "Arguments"; qid = smart_global; |