diff options
| -rw-r--r-- | src/Compilers/Reify.v | 2 | ||||
| -rw-r--r-- | src/Compilers/Z/Reify.v | 2 |
2 files changed, 2 insertions, 2 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. diff --git a/src/Compilers/Z/Reify.v b/src/Compilers/Z/Reify.v index 8fb02536d..7cb978241 100644 --- a/src/Compilers/Z/Reify.v +++ b/src/Compilers/Z/Reify.v @@ -92,7 +92,7 @@ Definition Interp_Reify_evar_package Ltac autosolve else_tac := lazymatch goal with | [ |- @Reify_evar_package _ _ ] - => eexists; cbv beta; Reify_rhs + => eexists; cbv beta; Reify_rhs; reflexivity | _ => Compilers.Reify.autosolve else_tac end. |