From 01704910babc7da4bb0591412cd1640338865751 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 2 Aug 2018 18:36:58 -0400 Subject: Better rewrite_type_transport_correct --- src/Experiments/NewPipeline/LanguageInversion.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') 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 -- cgit v1.2.3