diff options
Diffstat (limited to 'src/Compilers/Reify.v')
| -rw-r--r-- | src/Compilers/Reify.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Compilers/Reify.v b/src/Compilers/Reify.v index 715194baf..4454f2af2 100644 --- a/src/Compilers/Reify.v +++ b/src/Compilers/Reify.v @@ -536,7 +536,7 @@ Definition Interp_Reify_evar_package Ltac autosolve else_tac := lazymatch goal with | [ |- @Reify_evar_package ?base_type_code ?interp_base_type ?op ?make_const ?interp_op _ _ ] - => eexists; cbv beta; Reify_rhs base_type_code interp_base_type op make_const interp_op + => eexists; cbv beta; Reify_rhs base_type_code interp_base_type op make_const interp_op; reflexivity | _ => else_tac () end. |