diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-24 18:46:18 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-26 12:58:15 +0200 |
| commit | 81545ec98255e644be589d34a521924549e9e2fa (patch) | |
| tree | 65ab59d21e680a00e379deffa440f038b5d0c121 /parsing | |
| parent | 0f107c8a747af6bdb40d70d80236f84b325dc35d (diff) | |
[api] Move `hint_info_expr` to `Typeclasses`.
`hint_info_expr`, `hint_info_gen` do conceptually belong to the
typeclasses modules and should be able to be used without a dependency
on the concrete vernacular syntax.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 6 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 2dbd624c2..b3bc895ba 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -645,7 +645,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 @@ -770,8 +770,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] ] ] diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 9f186224b..0fbf2f567 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -260,7 +260,7 @@ module Vernac_ : val noedit_mode : vernac_expr Gram.entry val command_entry : vernac_expr Gram.entry val red_expr : raw_red_expr Gram.entry - val hint_info : Vernacexpr.hint_info_expr Gram.entry + val hint_info : Typeclasses.hint_info_expr Gram.entry end (** The main entry: reads an optional vernac command *) |