diff options
| author | Gaëtan Gilbert | 2020-08-24 13:11:08 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-08-25 16:10:30 +0200 |
| commit | 5e4d696c0a5c864092f7263b9bb7f7eb419d121e (patch) | |
| tree | 27bb191cd8e7ba35598e5d8c4a269e7fff6b8520 | |
| parent | 9b2979bc798dd6123bc4d599af3de894bff19c5b (diff) | |
elim.ml: stop using intro_using
| -rw-r--r-- | tactics/elim.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/elim.ml b/tactics/elim.ml index 415c980c2a..274ebc9f60 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -82,10 +82,10 @@ let general_decompose recognizer c = Proofview.Goal.enter begin fun gl -> let typc = pf_get_type_of gl c in tclTHENS (cut typc) - [ tclTHEN (intro_using tmphyp_name) - (onLastHypId - (ifOnHyp recognizer (general_decompose_aux recognizer) - (fun id -> clear [id]))); + [ intro_using_then tmphyp_name (fun id -> + ifOnHyp recognizer (general_decompose_aux recognizer) + (fun id -> clear [id]) + id); exact_no_check c ] end |