diff options
| author |  Jason Gross <jagro@google.com> | 2018-08-02 18:36:58 -0400 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2018-08-02 18:36:58 -0400 |
| commit | 01704910babc7da4bb0591412cd1640338865751 (patch) | |
| tree | 1644e99daf2a85c4b2b02f032d5e55039d48f603 /src | |
| parent | c3199e59f7c8d8e73e653808b50f77dc8e905b0a (diff) | |
Better rewrite_type_transport_correct
Diffstat (limited to 'src')
| -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 |