diff options
Diffstat (limited to 'vernac/g_vernac.mlg')
| -rw-r--r-- | vernac/g_vernac.mlg | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 6438b48e32..b2db64f74c 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -723,11 +723,11 @@ GRAMMAR EXTEND Gram { VernacContext (List.flatten c) } | IDENT "Instance"; namesup = instance_name; ":"; - expl = [ "!" -> { Decl_kinds.Implicit } | -> { Decl_kinds.Explicit } ] ; t = operconstr LEVEL "200"; + t = operconstr LEVEL "200"; info = hint_info ; props = [ ":="; "{"; r = record_declaration; "}" -> { Some (true,r) } | ":="; c = lconstr -> { Some (false,c) } | -> { None } ] -> - { VernacInstance (snd namesup,(fst namesup,expl,t),props,info) } + { VernacInstance (fst namesup,snd namesup,t,props,info) } | IDENT "Existing"; IDENT "Instance"; id = global; info = hint_info -> @@ -888,9 +888,9 @@ GRAMMAR EXTEND Gram (* Hack! Should be in grammar_ext, but camlp5 factorizes badly *) | IDENT "Declare"; IDENT "Instance"; id = ident_decl; bl = binders; ":"; - expl = [ "!" -> { Decl_kinds.Implicit } | -> { Decl_kinds.Explicit } ] ; t = operconstr LEVEL "200"; + t = operconstr LEVEL "200"; info = hint_info -> - { VernacDeclareInstance (bl, (id, expl, t), info) } + { VernacDeclareInstance (id, bl, t, info) } (* Should be in syntax, but camlp5 would not factorize *) | IDENT "Declare"; IDENT "Scope"; sc = IDENT -> |