diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-04 14:48:24 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-04 14:48:24 +0200 |
| commit | af19d08003173718c0f7c070d0021ad958fbe58d (patch) | |
| tree | e148de88bbc70d6cd1561dffba2f301181bbb2f5 /tactics | |
| parent | 90ac335a32afc6bbca5c11b7be7aabc1f7abb89b (diff) | |
| parent | 81545ec98255e644be589d34a521924549e9e2fa (diff) | |
Merge PR #7338: [api] Move `hint_info_expr` to `Typeclasses`.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 4 | ||||
| -rw-r--r-- | tactics/hints.ml | 4 | ||||
| -rw-r--r-- | tactics/hints.mli | 4 |
3 files changed, 6 insertions, 6 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 diff --git a/tactics/hints.ml b/tactics/hints.ml index 46d162911..739f1014a 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -28,12 +28,13 @@ open Termops open Inductiveops open Typing open Decl_kinds +open Vernacexpr +open Typeclasses open Pattern open Patternops open Clenv open Tacred open Printer -open Vernacexpr module NamedDecl = Context.Named.Declaration @@ -94,7 +95,6 @@ let secvars_of_hyps hyps = else pred let empty_hint_info = - let open Vernacexpr in { hint_priority = None; hint_pattern = None } (************************************************************************) diff --git a/tactics/hints.mli b/tactics/hints.mli index 1811150c2..b06ede0e1 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -31,7 +31,7 @@ type debug = Debug | Info | Off val secvars_of_hyps : ('c, 't) Context.Named.pt -> Id.Pred.t -val empty_hint_info : 'a hint_info_gen +val empty_hint_info : 'a Typeclasses.hint_info_gen (** Pre-created hint databases *) @@ -144,7 +144,7 @@ type hint_db = Hint_db.t type hnf = bool -type hint_info = (patvar list * constr_pattern) hint_info_gen +type hint_info = (patvar list * constr_pattern) Typeclasses.hint_info_gen type hint_term = | IsGlobRef of global_reference |