Changeset 1583 for src/common/Globalenvs.ma
 Timestamp:
 Dec 2, 2011, 1:02:08 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Globalenvs.ma
r1545 r1583 549 549 ?*) 550 550 . 551 552 lemma find_funct_find_funct_ptr : ∀F,ge,v,f. 553 find_funct Genv F ge v = Some F f → 554 ∃pty,b,c. v = Vptr (mk_pointer pty b c zero_offset) ∧ find_funct_ptr Genv F ge b = Some F f. 555 #F #ge * 556 [ #f #E normalize in E; destruct 557  #sz #i #f #E normalize in E; destruct 558  #f #fn #E normalize in E; destruct 559  #r #f #E normalize in E; destruct 560  * #pty #b #c * #off #f #E normalize in E; 561 cases off in E ⊢ %; [ 2,3: #x ] 562 #E normalize in E; destruct 563 %{pty} %{b} %{c} % // @E 564 ] qed. 565 551 566 (* 552 567 ##[ #A B C transf p b f; elim p; #fns main vars;
Note: See TracChangeset
for help on using the changeset viewer.