diff options
Diffstat (limited to 'src/Compilers/MapCastByDeBruijnWf.v')
| -rw-r--r-- | src/Compilers/MapCastByDeBruijnWf.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Compilers/MapCastByDeBruijnWf.v b/src/Compilers/MapCastByDeBruijnWf.v index 7c1e386b5..61a084ee7 100644 --- a/src/Compilers/MapCastByDeBruijnWf.v +++ b/src/Compilers/MapCastByDeBruijnWf.v @@ -64,6 +64,7 @@ Section language. then fun pf => left (base_type_code_bl_transparent _ _ pf) else fun pf => right _) eq_refl). { clear -pf base_type_code_lb. + let pf := pf in abstract (intro; erewrite base_type_code_lb in pf by eassumption; congruence). } Defined. |