- Timestamp:
- Nov 19, 2011, 12:38:20 AM (9 years ago)
- Location:
- src/joint
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/joint/BEValues.ma
r1395 r1516 74 74 [ O ⇒ λ_.[] 75 75 | S m ⇒ λpr':n=S m.(BVptr p (mk_part … part …))::bevals_of_pointer_aux p (S part) m ?] (refl ? n). 76 /3/ qed.76 /3/ (*Andrea: by _ cannot be re-parsed*) qed. 77 77 78 78 definition bevals_of_pointer: pointer → list beval ≝ … … 84 84 * * #pbl #pok #poff 85 85 try % 86 whd in ⊢ (??%?) >reflexive_eq_pointer >(eqb_n_n 1) [2,3: %]87 whd in ⊢ (??%?) >reflexive_eq_pointer >(eqb_n_n 2) %86 whd in ⊢ (??%?); >reflexive_eq_pointer >(eqb_n_n 1) [2,3: %] 87 whd in ⊢ (??%?); >reflexive_eq_pointer >(eqb_n_n 2) % 88 88 qed. 89 89 -
src/joint/TranslateUtils.ma
r1515 r1516 21 21 #pars0 #globals #def #n elim n 22 22 [ % 23 | #m whd in ⊢ (? → ??(??%)?) whd in ⊢ (? → ??(??match % with [ _ ⇒ ?])?)23 | #m whd in ⊢ (? → ??(??%)?); whd in ⊢ (? → ??(??match % with [ _ ⇒ ?])?) ; 24 24 cases (fresh_regs pars0 globals def m) normalize nodelta 25 #def' #regs #EQ change in EQ with (|regs| = m) <EQ25 #def' #regs #EQ change in EQ; with (|regs| = m) <EQ 26 26 @refl 27 27 ]
Note: See TracChangeset
for help on using the changeset viewer.