move implement_box_transformation to coq-malfunction

erasure-plugin/theories/ETransform.v

@@ -563,37 +563,3 @@ Proof.
   rewrite -eq.
   eapply transform_blocks_extends; eauto. apply pr. apply pr'.
 Qed.
-
-From MetaCoq.Erasure Require Import EImplementBox.
-
-Program Definition implement_box_transformation {efl : EEnvFlags}
-  {has_app : has_tApp} {has_letin : has_tLetIn} {has_cofix : has_tCoFix = false} {has_pars : has_cstr_params = false} {has_cstrblocks : cstr_as_blocks = true} :
-  Transform.t _ _ EAst.term EAst.term _ _ (eval_eprogram block_wcbv_flags) (eval_eprogram block_wcbv_flags) :=
-  {| name := "transforming to constuctors as blocks";
-    transform p _ := EImplementBox.implement_box_program p ;
-    pre p := wf_eprogram efl p ;
-    post p := wf_eprogram (switch_off_box efl) p ;
-    obseq p hp p' v v' := v' = implement_box v |}.
-
-Next Obligation.
-  intros. cbn in *. destruct p. split.
-  - eapply implement_box_env_wf_glob; eauto.   
-  - now eapply transform_wellformed'.
-Qed.
-Next Obligation.
-  red. intros. destruct pr. destruct H.
-  eexists. split; [ | eauto].
-  econstructor.
-  eapply implement_box_eval; cbn; eauto.
-Qed.
-
-#[global]
-Instance implement_box_extends (efl : EEnvFlags) {has_app : has_tApp} {has_letin : has_tLetIn} {has_cofix : has_tCoFix = false} {has_pars : has_cstr_params = false} {has_cstrblocks : cstr_as_blocks = true} :
-   TransformExt.t (implement_box_transformation (has_app := has_app) (has_letin := has_letin) (has_cofix := has_cofix) (has_pars := has_pars) (has_cstrblocks := has_cstrblocks)) extends_eprogram extends_eprogram.
-Proof.
-  red. intros p p' pr pr' [ext eq]. rewrite /transform /= /implement_box_program /=.
-  split => /=.
-  eapply (implement_box_env_extends has_app ext). apply pr. apply pr'.
-  now rewrite -eq.
-Qed.
-