diff options
| author | Pierre-Marie Pédrot | 2020-07-16 20:06:07 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-12 14:07:13 +0200 |
| commit | e28edfdc3c373af7f5ca4fbd716c8c5753494d5a (patch) | |
| tree | de91d924b1bbf492820d2e8dea65e3391a4b06bd /tactics/class_tactics.ml | |
| parent | a666788182bce7059e6ba41b917b5ca6ab52ae13 (diff) | |
Export a dedicated function that applies immediately a hint.
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 279476badb..62470a60c0 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -170,10 +170,7 @@ let e_give_exact flags h = let unify_resolve ~with_evars flags h diff = match diff with | None -> - Proofview.Goal.enter begin fun gls -> - let clenv', _ = connect_hint_clenv h gls in - Clenv.res_pf ~with_evars ~with_classes:false ~flags clenv' - end + Hints.hint_res_pf ~with_evars ~with_classes:false ~flags h | Some (diff, ty) -> let () = assert (not h.hint_poly) in Proofview.Goal.enter begin fun gl -> |