diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/lemmas.ml | 2 |
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 |