Putting all the tactics exported by the Tactics module in the new monad API.

1 files changed, 1 insertions, 1 deletions

diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 80b3fef196..ce5ef01699 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -403,7 +403,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
     | Anonymous -> Tactics.intro) (List.rev ids) in
   let init_tac,guard = match recguard with
   | Some (finite,guard,init_tac) ->
-      let rec_tac = Proofview.V82.tactic (rec_tac_initializer finite guard thms snl) in
+      let rec_tac = rec_tac_initializer finite guard thms snl in
       Some (match init_tac with
         | None -> 
             if Flags.is_auto_intros () then