diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 4504146258..aac47126fc 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -560,10 +560,12 @@ GEXTEND Gram ":="; c = lconstr -> Some c | -> None ] -> VernacInstance (false,snd namesup,(fst namesup,expl,t),props,pri) - | IDENT "Existing"; IDENT "Instance"; id = global -> - VernacDeclareInstances [id] - | IDENT "Existing"; IDENT "Instances"; ids = LIST1 global -> - VernacDeclareInstances ids + | IDENT "Existing"; IDENT "Instance"; id = global; + pri = OPT [ "|"; i = natural -> i ] -> + VernacDeclareInstances ([id], pri) + | IDENT "Existing"; IDENT "Instances"; ids = LIST1 global; + pri = OPT [ "|"; i = natural -> i ] -> + VernacDeclareInstances (ids, pri) | IDENT "Existing"; IDENT "Class"; is = global -> VernacDeclareClass is |