diff options
| -rw-r--r-- | src/Reflection/Reify.v | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/src/Reflection/Reify.v b/src/Reflection/Reify.v index 3606cae99..c83d15fe8 100644 --- a/src/Reflection/Reify.v +++ b/src/Reflection/Reify.v @@ -264,14 +264,15 @@ Ltac Reify_rhs_gen Reify prove_interp_compile_correct interp_op try_tac := including the parameterized bits; we assume that [hnf] is enough to unfold the interpretation functions that we're parameterized over. *) - lazymatch goal with - | [ |- ?R (@InputSyntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op ?t ?e) _ ] - => let interp_base_type' := (eval hnf in interp_base_type) in - let interp_op' := (eval hnf in interp_op) in - change interp_base_type with interp_base_type'; - change interp_op with interp_op' - end; - cbv iota beta delta [InputSyntax.Interp interp_type interp_type_gen interp_flat_type interp interpf]; simplify_projections; reflexivity) ] ] ]. + abstract ( + lazymatch goal with + | [ |- ?R (@InputSyntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op ?t ?e) _ ] + => let interp_base_type' := (eval hnf in interp_base_type) in + let interp_op' := (eval hnf in interp_op) in + change interp_base_type with interp_base_type'; + change interp_op with interp_op' + end; + cbv iota beta delta [InputSyntax.Interp interp_type interp_type_gen interp_flat_type interp interpf]; reflexivity)) ] ] ]. Ltac prove_compile_correct := fun _ => lazymatch goal with |