diff options
Diffstat (limited to 'src/Reflection/Z/MapCastByDeBruijnInterp.v')
| -rw-r--r-- | src/Reflection/Z/MapCastByDeBruijnInterp.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Reflection/Z/MapCastByDeBruijnInterp.v b/src/Reflection/Z/MapCastByDeBruijnInterp.v index 072563680..6e57136ab 100644 --- a/src/Reflection/Z/MapCastByDeBruijnInterp.v +++ b/src/Reflection/Z/MapCastByDeBruijnInterp.v @@ -44,7 +44,7 @@ Section language. Interp interp_op_bounds e input_bounds = b /\ @inbounds _ b (Interp interp_op e v) /\ cast_back _ _ (Interp interp_op e' v') = (Interp interp_op e v). - Proof. + Proof using Type*. apply MapCastCorrect; auto using internal_base_type_dec_lb. Qed. End language. |