diff options
Diffstat (limited to 'src/Compilers/MapCastByDeBruijnInterp.v')
| -rw-r--r-- | src/Compilers/MapCastByDeBruijnInterp.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Compilers/MapCastByDeBruijnInterp.v b/src/Compilers/MapCastByDeBruijnInterp.v index 10e09242a..7674e5f0e 100644 --- a/src/Compilers/MapCastByDeBruijnInterp.v +++ b/src/Compilers/MapCastByDeBruijnInterp.v @@ -66,6 +66,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. |