diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/NewPipeline/RewriterWf1.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Experiments/NewPipeline/RewriterWf1.v b/src/Experiments/NewPipeline/RewriterWf1.v index a244fa1b4..8200a131c 100644 --- a/src/Experiments/NewPipeline/RewriterWf1.v +++ b/src/Experiments/NewPipeline/RewriterWf1.v @@ -781,7 +781,7 @@ Module Compilers. : @unify_types ident var pident t e p T k = k (@unify_types ident var pident t e p _ id). Proof using Type. cbv [unify_types]; break_innermost_match; try reflexivity. - etransitivity; rewrite pattern.type.add_var_types_cps_id; reflexivity. + etransitivity; rewrite pattern.type.add_var_types_cps_id; [ reflexivity | ]; break_innermost_match; reflexivity. Qed. Lemma unify_pattern'_cps_id {t e p evm K v T cont} |