From 5e4d696c0a5c864092f7263b9bb7f7eb419d121e Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 24 Aug 2020 13:11:08 +0200
Subject: elim.ml: stop using intro_using

---
 tactics/elim.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'tactics')

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
 
-- 
cgit v1.2.3