From 5bff961f39ec8bf755030f9fbc1acc15bbc265c6 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 30 May 2018 15:55:46 +0200 Subject: Small refactoring to clarify make_local_hint_db. --- tactics/hints.ml | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/tactics/hints.ml b/tactics/hints.ml index 786760122..1e1b0d5be 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1361,12 +1361,10 @@ let expand_constructor_hints env sigma lems = (* builds a hint database from a constr signature *) (* typically used with (lid, ltyp) = pf_hyps_types *) -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 @@ -1377,8 +1375,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 -- cgit v1.2.3