Changeset 1521 for src/Cminor
- Timestamp:
- Nov 21, 2011, 1:06:01 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Cminor/toRTLabs.ma
r1516 r1521 28 28 whd in E:(??%?); destruct; 29 29 whd >lookup_add_hit % #A destruct 30 | #H change in E:(??(match % with [ _ ⇒ ? ])?); with (populate_env e u tl)30 | #H change with (populate_env e u tl) in E:(??(match % with [ _ ⇒ ? ])?); 31 31 lapply (refl ? (populate_env e u tl)) 32 32 cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); (* XXX if I do this directly it rewrites both sides of the equality *) … … 44 44 [ #e #u #l' #e' #u' #E whd in E:(??%?); destruct // 45 45 | * #id #t #tl #IH #e #u #l' #e' #u' #E whd in E:(??%?); 46 change in E:(??(match % with [ _ ⇒ ?])?); with (populate_env e u tl)46 change with (populate_env e u tl) in E:(??(match % with [ _ ⇒ ?])?); 47 47 lapply (refl ? (populate_env e u tl)) 48 48 cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); * #l0 #e0 #u0 #E0 … … 65 65 [ #lbls #u #lbls' #u' #E #l * 66 66 | #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?); 67 change in ⊢ (??match % with [ _ ⇒ ? ]? → ?); with (populate_label_env ???)67 change with (populate_label_env ???) in ⊢ (??match % with [ _ ⇒ ? ]? → ?); 68 68 lapply (refl ? (populate_label_env lbls u t)) 69 69 cases (populate_label_env lbls u t) in ⊢ (???% → %); … … 82 82 [ #lbls #u #lbls' #u' #E #l #H %2 whd in E:(??%?); destruct @H 83 83 | #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?); 84 change in ⊢ (??match % with [ _ ⇒ ? ]? → ?); with (populate_label_env ???)84 change with (populate_label_env ???) in ⊢ (??match % with [ _ ⇒ ? ]? → ?); 85 85 lapply (refl ? (populate_label_env lbls u t)) 86 86 cases (populate_label_env lbls u t) in ⊢ (???% → %);
Note: See TracChangeset
for help on using the changeset viewer.