diff options
author | Jason Gross <jgross@mit.edu> | 2017-11-12 07:56:26 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-11-12 18:07:52 -0500 |
commit | 9f7c3c49118b907b713de3525ede966d4bd5d048 (patch) | |
tree | 7f7660e96dd7f4cd9f817f86afc28fc524e9dac3 | |
parent | 4cfc0a4e8037fde12a18434cd6c229db14d4b9e5 (diff) |
add reflexivity to reify autosolve
-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. |