diff options
Diffstat (limited to 'vernac/g_vernac.mlg')
| -rw-r--r-- | vernac/g_vernac.mlg | 17 |
1 files changed, 8 insertions, 9 deletions
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 22528a607f..3bc4aecdb1 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -683,19 +683,19 @@ GRAMMAR EXTEND Gram info = hint_info ; props = [ ":="; "{"; r = record_declaration; "}" -> { Some (true,r) } | ":="; c = lconstr -> { Some (false,c) } | -> { None } ] -> - { VernacInstance (false,snd namesup,(fst namesup,expl,t),props,info) } + { VernacInstance (snd namesup,(fst namesup,expl,t),props,info) } | IDENT "Existing"; IDENT "Instance"; id = global; info = hint_info -> - { VernacDeclareInstances [id, info] } + { VernacExistingInstance [id, info] } | IDENT "Existing"; IDENT "Instances"; ids = LIST1 global; pri = OPT [ "|"; i = natural -> { i } ] -> { let info = { Typeclasses.hint_priority = pri; hint_pattern = None } in let insts = List.map (fun i -> (i, info)) ids in - VernacDeclareInstances insts } + VernacExistingInstance insts } - | IDENT "Existing"; IDENT "Class"; is = global -> { VernacDeclareClass is } + | IDENT "Existing"; IDENT "Class"; is = global -> { VernacExistingClass is } (* Arguments *) | IDENT "Arguments"; qid = smart_global; @@ -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: @@ -845,10 +844,10 @@ GRAMMAR EXTEND Gram [ [ IDENT "Comments"; l = LIST0 comment -> { VernacComments l } (* Hack! Should be in grammar_ext, but camlp5 factorizes badly *) - | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":"; + | IDENT "Declare"; IDENT "Instance"; id = ident_decl; bl = binders; ":"; expl = [ "!" -> { Decl_kinds.Implicit } | -> { Decl_kinds.Explicit } ] ; t = operconstr LEVEL "200"; info = hint_info -> - { VernacInstance (true, snd namesup, (fst namesup, expl, t), None, info) } + { VernacDeclareInstance (bl, (id, expl, t), info) } (* Should be in syntax, but camlp5 would not factorize *) | IDENT "Declare"; IDENT "Scope"; sc = IDENT -> |