diff options
Diffstat (limited to 'src/RewriterRulesInterpGood.v')
| -rw-r--r-- | src/RewriterRulesInterpGood.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/RewriterRulesInterpGood.v b/src/RewriterRulesInterpGood.v index 469f0cb31..612f72afd 100644 --- a/src/RewriterRulesInterpGood.v +++ b/src/RewriterRulesInterpGood.v @@ -743,6 +743,13 @@ Module Compilers. Time all: try solve [ repeat interp_good_t_step_related; repeat interp_good_t_step_arith; fin_with_nia ]. Qed. + Lemma strip_literal_casts_rewrite_rules_interp_good + : rewrite_rules_interp_goodT strip_literal_casts_rewrite_rules. + Proof using Type. + Time start_interp_good. + Time all: try solve [ repeat interp_good_t_step_related; repeat interp_good_t_step_arith ]. + Qed. + Local Ltac fancy_local_t := repeat match goal with | [ H : forall s v v', ?invert_low s v = Some v' -> v = _, |