diff options
Diffstat (limited to 'src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v')
| -rw-r--r-- | src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v b/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v index 3e38eabdf..38ed60038 100644 --- a/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v +++ b/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v @@ -160,7 +160,7 @@ Section with_round_up. | progress destruct_head'_and ]; [ | rewrite cast_const_idempotent_small by t_small; reflexivity - | ]; + | .. ]; repeat match goal with | _ => progress change (@cast_const TZ) with @ZToInterp in * | [ |- context[@cast_const ?x TZ] ] |