Changeset 3586
- Timestamp:
- Jul 18, 2015, 6:39:51 PM (6 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
LTS/variable_stack_pass.ma
r3585 r3586 461 461 inversion(divide_continuation_on_frames ct [i]) 462 462 #IH normalize nodelta whd in ⊢(?→%→%); [#_|3:#ABS cases ABS] 463 [>IH whd in match (frame_assign_var ???); #HN 463 [>IH whd in match (frame_assign_var ???); inversion(new_st) 464 #l #p #Hns #HN] 464 465 cases daemon 465 466 qed. … … 469 470 var_instr_bond_ok st (SEQ … seq opt_l i) ct → 470 471 var_instr_bond_ok st i ct. 472 * [|#x #xs] #i #seq #ol #ct whd in ⊢(%→?); inversion(divide_continuation_on_frames ct ?) 473 normalize nodelta [2: #H1 #H2 #H3 #H4|3:#H] [1,2:#ABS cases ABS] 474 cases i whd in match(var_instr_bond_ok ??); inversion(ct) 475 [1,3,5,7: whd in match(var_instr_bond_ok ???);] 476 [#_ whd in match(divide_continuation_on_frames ??); 477 #ABS destruct| #H1 #H2 whd in match (divide_continuation_on_frames ??); 478 #ABS destruct| #H1 #H2 #H3 #H4 whd in match (divide_continuation_on_frames ??); #ABS destruct 479 |#H8 #H9 #H10 #H11 #H12 #H13 #H14 whd in match (divide_continuation_on_frames ??); #ABS destruct 480 |* #fl #fi #H10 cases fl [#fn #ccl|2,3:#op] #H20 [2,3:#H21 whd in match (divide_continuation_on_frames ??); 481 #ABS destruct|whd in match (divide_continuation_on_frames ??); 482 #H29 cases H10 [2:#al #l] whd in match (divide_continuation_on_frames ??); 483 [2:#ABS destruct 484 |1: whd in match(var_instr_bond_ok …); 485 ] 486 ] 487 ] 488 471 489 cases daemon 472 490 qed.
Note: See TracChangeset
for help on using the changeset viewer.