Commit ee9d4038 authored by Dan Frumin's avatar Dan Frumin
Browse files

Fix compilation

parent 1750671e
......@@ -429,7 +429,6 @@ Section vcg_spec.
destruct d as [i|?]; simplify_eq/=.
destruct (vcg_sp E mIn1 mOut1 de2) as [[[[mIn2 mOut2] mNew2] dv2]|] eqn:Hsp2; simplify_eq /=.
destruct (denv_delete_full_3 i mIn2 mOut2 (denv_merge mNew1 mNew2)) as [[[[mIn3 mOut3] mNew3] dv1]|] eqn:Hout1; simplify_eq/=.
apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
destruct (IHde1 _ _ _ _ _ _ HwfIn HwfOut Hwfde1 Hsp1) as (HwfIn1&HwfOut1&HwfNew1&Hwfdv1).
destruct (IHde2 _ _ _ _ _ _ HwfIn1 HwfOut1 Hwfde2 Hsp2) as (?&?&?&?).
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment