diff options
Diffstat (limited to 'src/Reflection/Reify.v')
| -rw-r--r-- | src/Reflection/Reify.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Reflection/Reify.v b/src/Reflection/Reify.v index ce6a8db08..3606cae99 100644 --- a/src/Reflection/Reify.v +++ b/src/Reflection/Reify.v @@ -265,7 +265,7 @@ Ltac Reify_rhs_gen Reify prove_interp_compile_correct interp_op try_tac := [hnf] is enough to unfold the interpretation functions that we're parameterized over. *) lazymatch goal with - | [ |- @InputSyntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op ?t ?e = _ ] + | [ |- ?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'; |