diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-04 10:16:10 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-04 10:16:10 +0200 |
| commit | 25b394bf06c2186af719609e284ebb0df9573569 (patch) | |
| tree | 592ff8c4329a2a6dd0451ede63e3aa51b697fa3e /tactics | |
| parent | 73209b57ecdf0ad7e00087cf86b94ba9ab858088 (diff) | |
| parent | 5bff961f39ec8bf755030f9fbc1acc15bbc265c6 (diff) | |
Merge PR #7640: Small refactoring to clarify make_local_hint_db.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/hints.ml | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index a86103d57..636edeb34 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1379,12 +1379,10 @@ let expand_constructor_hints env sigma lems = (* builds a hint database from a constr signature *) (* typically used with (lid, ltyp) = pf_hyps_types <some goal> *) -let add_hint_lemmas env sigma eapply lems hint_db = +let constructor_hints env sigma eapply lems = let lems = expand_constructor_hints env sigma lems in - let hintlist' = - List.map_append (fun (poly, lem) -> - make_resolves env sigma (eapply,true,false) empty_hint_info poly lem) lems in - Hint_db.add_list env sigma hintlist' hint_db + List.map_append (fun (poly, lem) -> + make_resolves env sigma (eapply,true,false) empty_hint_info poly lem) lems let make_local_hint_db env sigma ts eapply lems = let map c = c env sigma in @@ -1395,8 +1393,9 @@ let make_local_hint_db env sigma ts eapply lems = | Some ts -> ts in let hintlist = List.map_append (make_resolve_hyp env sigma) sign in - add_hint_lemmas env sigma eapply lems - (Hint_db.add_list env sigma hintlist (Hint_db.empty ts false)) + Hint_db.empty ts false + |> Hint_db.add_list env sigma hintlist + |> Hint_db.add_list env sigma (constructor_hints env sigma eapply lems) let make_local_hint_db env sigma ?ts eapply lems = make_local_hint_db env sigma ts eapply lems |