diff options
Diffstat (limited to 'src/Experiments/NewPipeline/UnderLetsProofs.v')
| -rw-r--r-- | src/Experiments/NewPipeline/UnderLetsProofs.v | 2 |
1 files changed, 2 insertions, 0 deletions
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. |