diff options
Diffstat (limited to 'src/Experiments/NewPipeline/LanguageInversion.v')
-rw-r--r-- | src/Experiments/NewPipeline/LanguageInversion.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Experiments/NewPipeline/LanguageInversion.v b/src/Experiments/NewPipeline/LanguageInversion.v index b0db97e75..d00efa46c 100644 --- a/src/Experiments/NewPipeline/LanguageInversion.v +++ b/src/Experiments/NewPipeline/LanguageInversion.v @@ -327,7 +327,7 @@ Module Compilers. end. Ltac rewrite_type_transport_correct := - cbv [type.try_transport_cps type.try_transport base.try_transport] in *; + cbv [type.try_transport_cps type.try_transport base.try_transport base.try_transport_cps] in *; cbn [type.try_make_transport_cps] in *; cbv [cpscall cpsbind cps_option_bind cpsreturn id] in *; repeat match goal with |