diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 3026be248..a1c563f53 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -646,7 +646,7 @@ GEXTEND Gram | IDENT "Existing"; IDENT "Instances"; ids = LIST1 global; pri = OPT [ "|"; i = natural -> i ] -> - let info = { hint_priority = pri; hint_pattern = None } in + let info = { Typeclasses.hint_priority = pri; hint_pattern = None } in let insts = List.map (fun i -> (i, info)) ids in VernacDeclareInstances insts @@ -771,8 +771,8 @@ GEXTEND Gram ; hint_info: [ [ "|"; i = OPT natural; pat = OPT constr_pattern -> - { hint_priority = i; hint_pattern = pat } - | -> { hint_priority = None; hint_pattern = None } ] ] + { Typeclasses.hint_priority = i; hint_pattern = pat } + | -> { Typeclasses.hint_priority = None; hint_pattern = None } ] ] ; reserv_list: [ [ bl = LIST1 reserv_tuple -> bl | b = simple_reserv -> [b] ] ] |