diff options
Diffstat (limited to 'vernac/g_vernac.mlg')
| -rw-r--r-- | vernac/g_vernac.mlg | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index dfc7b05b51..4c08cf7f79 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -687,7 +687,7 @@ GRAMMAR EXTEND Gram { VernacContext (List.flatten c) } | IDENT "Instance"; namesup = instance_name; ":"; - t = operconstr LEVEL "200"; + t = term LEVEL "200"; info = hint_info ; props = [ ":="; "{"; r = record_declaration; "}" -> { Some (true,r) } | ":="; c = lconstr -> { Some (false,c) } | -> { None } ] -> @@ -837,7 +837,7 @@ GRAMMAR EXTEND Gram (* Hack! Should be in grammar_ext, but camlp5 factorizes badly *) | IDENT "Declare"; IDENT "Instance"; id = ident_decl; bl = binders; ":"; - t = operconstr LEVEL "200"; + t = term LEVEL "200"; info = hint_info -> { VernacDeclareInstance (id, bl, t, info) } |