diff options
Diffstat (limited to 'src/Compilers/Named/FMapContext.v')
| -rw-r--r-- | src/Compilers/Named/FMapContext.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/Compilers/Named/FMapContext.v b/src/Compilers/Named/FMapContext.v index 02b0fd05c..b69d78d09 100644 --- a/src/Compilers/Named/FMapContext.v +++ b/src/Compilers/Named/FMapContext.v @@ -49,7 +49,9 @@ Module FMapContextFun (E : DecidableType) (W : WSfun E). | progress break_innermost_match_step | rewrite concat_pV | congruence - | rewrite base_type_code_lb in * by reflexivity ]. + | rewrite base_type_code_lb in * by reflexivity + | break_innermost_match_hyps_step + | progress unfold var_cast in * ]. Qed. End ctx. |