diff options
| author | Pierre-Marie Pédrot | 2016-05-17 22:37:19 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-17 22:38:40 +0200 |
| commit | f7fb1918619fcef384d4aa84938246de67c707fa (patch) | |
| tree | 6f8b1b8ba71681b06b4a74ddeee76d02a3ef09dd /plugins/romega | |
| parent | cead0ce54cf290016e088ee7f203d327a3eea957 (diff) | |
| parent | dadd4003b6607ccc103658f842b5efbd6d8ab57f (diff) | |
Putting all the tactics exported by the Tactics module in the new monad API.
Diffstat (limited to 'plugins/romega')
| -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 177c870b3c..dca46cbcf7 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 >> |