From b3184e2f2e26524181b7e58bb7b0b95e34543184 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 31 Jul 2018 11:23:37 -0400 Subject: Comment out wf_splice_list It wasn't actually ready yet --- src/Experiments/NewPipeline/UnderLetsProofs.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src') diff --git a/src/Experiments/NewPipeline/UnderLetsProofs.v b/src/Experiments/NewPipeline/UnderLetsProofs.v index bc97dd809..ba4e0aa2c 100644 --- a/src/Experiments/NewPipeline/UnderLetsProofs.v +++ b/src/Experiments/NewPipeline/UnderLetsProofs.v @@ -232,6 +232,7 @@ Module Compilers. eauto using (ex_intro _ nil). Qed. + (* Lemma wf_splice_list {A1 B1 A2 B2} {P : list { t : type & var1 t * var2 t }%type -> A1 -> A2 -> Prop} {Q : list { t : type & var1 t * var2 t }%type -> B1 -> B2 -> Prop} @@ -250,6 +251,7 @@ Module Compilers. rewrite ListUtil.app_cons_app_app in *. eauto using (ex_intro _ nil). Qed. + *) End with_var. End with_ident. -- cgit v1.2.3