diff options
author | Jason Gross <jgross@mit.edu> | 2016-10-30 13:26:18 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-10-30 13:26:18 -0400 |
commit | b135710a39bed142c796ea675205f8881aa5b3a3 (patch) | |
tree | ae1d3880115db16aec2de87b9e2a652eb46f82df | |
parent | 15a026fc6aead83edd616ffd870a383a8d0d1210 (diff) |
Fix slowness in [Defined] after [Reify_rhs]
Do this by removing simplify_projections, which was messing with kernel reduction
-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 |