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 /tactics/class_tactics.ml | |
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 'tactics/class_tactics.ml')
-rw-r--r-- | tactics/class_tactics.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index b11e36bce..bbcf8def6 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -547,9 +547,9 @@ let make_resolve_hyp env sigma st flags only_classes pri decl = (List.map_append (fun (path,info,c) -> let info = - { info with Vernacexpr.hint_pattern = + { info with hint_pattern = Option.map (Constrintern.intern_constr_pattern env sigma) - info.Vernacexpr.hint_pattern } + info.hint_pattern } in make_resolves env sigma ~name:(PathHints path) (true,false,not !Flags.quiet) info false |