funind: stop using intro_using

2 files changed, 20 insertions, 7 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 743afe4177..72e6006b7e 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -483,7 +483,10 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos g =
         (Proofview.V82.of_tactic
            (intro_avoiding (Id.Set.of_list dyn_infos.rec_hyps)))
     ; (* Then the equation itself *)
-      Proofview.V82.of_tactic (intro_using heq_id)
+      Proofview.V82.of_tactic
+        (intro_using_then heq_id
+           (* we get the fresh name with onLastHypId *)
+           (fun _ -> Proofview.tclUNIT ()))
     ; onLastHypId (fun heq_id ->
           tclTHENLIST
             [ (* Then the new hypothesis *)
@@ -1113,16 +1116,18 @@ let prove_princ_for_struct (evd : Evd.evar_map ref) interactive_proof fun_num
   in
   let first_tac : tactic =
     (* every operations until fix creations *)
+    (* names are already refreshed *)
     tclTHENLIST
       [ observe_tac "introducing params"
           (Proofview.V82.of_tactic
-             (intros_using (List.rev_map id_of_decl princ_info.params)))
+             (intros_mustbe_force (List.rev_map id_of_decl princ_info.params)))
       ; observe_tac "introducing predictes"
           (Proofview.V82.of_tactic
-             (intros_using (List.rev_map id_of_decl princ_info.predicates)))
+             (intros_mustbe_force
+                (List.rev_map id_of_decl princ_info.predicates)))
       ; observe_tac "introducing branches"
           (Proofview.V82.of_tactic
-             (intros_using (List.rev_map id_of_decl princ_info.branches)))
+             (intros_mustbe_force (List.rev_map id_of_decl princ_info.branches)))
       ; observe_tac "building fixes" mk_fixes ]
   in
   let intros_after_fixes : tactic =
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 253c95fa67..066ade07d2 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -414,7 +414,8 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
   observe_tclTHENLIST
     (fun _ _ -> str "treat_case1")
     [ h_intros (List.rev rev_ids)
-    ; Proofview.V82.of_tactic (intro_using teq_id)
+    ; Proofview.V82.of_tactic
+        (intro_using_then teq_id (fun _ -> Proofview.tclUNIT ()))
     ; onLastHypId (fun heq ->
           observe_tclTHENLIST
             (fun _ _ -> str "treat_case2")
@@ -601,7 +602,11 @@ let rec destruct_bounds_aux infos (bound, hyple, rechyps) lbounds g =
                        (Proofview.V82.of_tactic (simplest_case (mkVar id)))
                        [ observe_tclTHENLIST
                            (fun _ _ -> str "")
-                           [ Proofview.V82.of_tactic (intro_using h_id)
+                           [ Proofview.V82.of_tactic
+                               (intro_using_then h_id
+                                  (* We don't care about the refreshed name,
+                                     accessed only through auto? *)
+                                  (fun _ -> Proofview.tclUNIT ()))
                            ; Proofview.V82.of_tactic
                                (simplest_elim
                                   (mkApp (delayed_force lt_n_O, [|s_max|])))
@@ -865,7 +870,10 @@ let terminate_app_rec (f, args) expr_info continuation_tac _ g =
             (simplest_elim (mkApp (mkVar expr_info.ih, Array.of_list args))))
          [ observe_tclTHENLIST
              (fun _ _ -> str "terminate_app_rec2")
-             [ Proofview.V82.of_tactic (intro_using rec_res_id)
+             [ Proofview.V82.of_tactic
+                 (intro_using_then rec_res_id
+                    (* refreshed name gotten from onNthHypId *)
+                    (fun _ -> Proofview.tclUNIT ()))
              ; Proofview.V82.of_tactic intro
              ; onNthHypId 1 (fun v_bound ->
                    onNthHypId 2 (fun v ->