diff options
Diffstat (limited to 'src/Experiments/NewPipeline/RewriterWf2.v')
| -rw-r--r-- | src/Experiments/NewPipeline/RewriterWf2.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Experiments/NewPipeline/RewriterWf2.v b/src/Experiments/NewPipeline/RewriterWf2.v index 6b2d92971..de17f2896 100644 --- a/src/Experiments/NewPipeline/RewriterWf2.v +++ b/src/Experiments/NewPipeline/RewriterWf2.v @@ -799,7 +799,7 @@ Module Compilers. => rewrite ap_transport_Base | [ |- True ] => exact I end - | progress cbv [wf_rewrite_rule_data wf_with_unif_rewrite_ruleTP_gen option_bind'] in * + | progress cbv [wf_rewrite_rule_data wf_with_unif_rewrite_ruleTP_gen option_bind' normalize_deep_rewrite_rule_cps_id_hypsT] in * | lazymatch goal with | [ |- (@unify_pattern1 ?t ?re1 ?p ?K1 ?v1 ?T1 ?cont1 = None <-> @unify_pattern2 ?t ?re2 ?p ?K2 ?v2 ?T2 ?cont2 = None) |