From b135710a39bed142c796ea675205f8881aa5b3a3 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 30 Oct 2016 13:26:18 -0400 Subject: Fix slowness in [Defined] after [Reify_rhs] Do this by removing simplify_projections, which was messing with kernel reduction --- src/Reflection/Reify.v | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) (limited to 'src/Reflection') 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 -- cgit v1.2.3