diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-30 15:55:46 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-30 15:55:46 +0200 |
| commit | 5bff961f39ec8bf755030f9fbc1acc15bbc265c6 (patch) | |
| tree | db780f8dedcbb603c89e7c4b52856ba6572a0aef /tactics | |
| parent | 853917631d58226d9669af64203901e2b19ed304 (diff) | |
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 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 <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 @@ -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 |