`Split_vc` takes a lot of time when used in huge context
Split_vc
uses substitution which have a bad behavior with huge context.
let simplify_intros =
Trans.compose introduce_premises
(Subst.subst_filtered ~subst_proxy:false subst_filter)
let split_vc =
Trans.compose_l
(*** do test:
(Trans.compose Simplify_formula.simplify_trivial_wp_quantification
*)
(Trans.compose generalize_intro Split_goal.split_goal_right)
(Trans.singleton simplify_intros)
We are trying to create a toy example, but in any case it seems strange that split_vc
looks at all the task. What is the goal os this substitution?
The lot of time is that a reload in the IDE can take 14min.