diff options
Diffstat (limited to 'plugins/romega/refl_omega.ml')
| -rw-r--r-- | plugins/romega/refl_omega.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 177c870b3..dca46cbcf 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -1280,8 +1280,8 @@ let resolution env full_reified_goal systems_list = CCHyp{o_hyp=id_concl;o_path=[]} :: hyp_stated_vars @ initial_context in let decompose_tactic = decompose_tree env context solution_tree in - Tactics.generalize - (l_generalize_arg @ List.map Term.mkVar (List.tl l_hyps)) >> + Proofview.V82.of_tactic (Tactics.generalize + (l_generalize_arg @ List.map Term.mkVar (List.tl l_hyps))) >> Proofview.V82.of_tactic (Tactics.change_concl reified) >> Proofview.V82.of_tactic (Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|])) >> show_goal >> |