diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-30 12:54:31 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-30 12:54:31 -0400 |
| commit | 15a026fc6aead83edd616ffd870a383a8d0d1210 (patch) | |
| tree | 33052846c888a8566034bdd3225df937fc52d739 /src/Reflection/Reify.v | |
| parent | 5bef18ca16a008e49b7b7bca5f7920149bd1bbaf (diff) | |
Make Z Reification handle correctness proofs
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'; |