Fix slowness in [Defined] after [Reify_rhs]

Do this by removing simplify_projections, which was messing with kernel reduction

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