Changeset 1515 for src/Clight/toCminor.ma
- Timestamp:
- Nov 18, 2011, 1:03:14 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/toCminor.ma
r1369 r1515 125 125 cases (identifier_eq ? id id') 126 126 [ #E >E >lookup_add_hit whd in ⊢ (% → ?) * 127 | #NE >lookup_add_miss / / @eq_identifier_elim // #E >E in NE * /2/127 | #NE >lookup_add_miss /2/ 128 128 ] qed. 129 129 … … 134 134 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ] → match % with [ _ ⇒ ? | _ ⇒ ? ]) 135 135 >lookup_add_miss 136 [ #H @H | @eq_identifier_elim // #E >E in NE */2/ ]136 [ #H @H | /2/ ] 137 137 qed. 138 138 … … 737 737 〈tmp,u'〉 = alloc_tmp q u → tmps_preserved vars u u'. 738 738 #tmp #g #g' #vars #q 739 whd in ⊢ (???% → ?) 740 generalize in ⊢ (???(match % with [ _ ⇒ ? ]) → ?) 741 * #tmp' #u whd in ⊢ (???% → ?) #E 742 destruct 739 whd in ⊢ (???% → ?) #E 743 740 #id #H 741 cases (identifier_eq ? id tmp) 742 destruct #E 744 743 whd in ⊢ (?%?) whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ] 745 cases (identifier_eq ? id tmp') 746 [ #E1 >E1 >lookup_add_hit @I 747 | * #NE >lookup_add_miss [ @H | @eq_identifier_elim // #E1 cases (NE E1) 744 [ >E >lookup_add_hit @I 745 | cases E #NE >lookup_add_miss [ @H | /2/ 748 746 ] qed. 749 747 … … 770 768 cases (identifier_eq ? id id') 771 769 [ #E >E >lookup_add_hit @I 772 | * #NE >lookup_add_miss [ @H | @eq_identifier_elim // #E cases (NE E)770 | #NE >lookup_add_miss [ @H | /2/ 773 771 ] qed. 774 772 … … 793 791 〈tmp,u〉 = alloc_tmp q u0 → local_id (add_tmps vars u) tmp. 794 792 #tmp #u #q #u0 #vars 795 whd in ⊢ (???% → ?) 796 generalize in ⊢ (???(match % with [ _ ⇒ ? ]) → ?) 797 * #tmp' #u' whd in ⊢ (???% → ?) #E 793 whd in ⊢ (???% → ?) #E 798 794 destruct 799 795 whd in ⊢ (?%?) whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ] >lookup_add_hit … … 997 993 l0 ≠ l → 998 994 lookup_label (add … lbls l l') l0 = lookup_label lbls l0. 999 #lbls #l #l' #l0 *#NE995 #lbls #l #l' #l0 #NE 1000 996 whd in ⊢ (??%%) 1001 997 >lookup_add_miss 1002 [ @refl | @(eq_identifier_elim ?? l0 l) 1003 [ #E cases (NE E) 1004 | #_ @I 1005 ] 1006 ] 998 [ @refl | @NE ] 1007 999 qed. 1008 1000 … … 1048 1040 cases (identifier_eq ? i id) 1049 1041 [ #E >E #H %2 whd %1 @refl 1050 | *#NE #H cases (IH ?)1042 | #NE #H cases (IH ?) 1051 1043 [ #H' %1 @H' 1052 1044 | #H' %2 %2 @H' 1053 1045 | whd in H; whd in H:(match % with [ _ ⇒ ? | _ ⇒ ? ]); 1054 >lookup_add_miss in H; [ #H @H | @ eq_identifier_elim // #E cases (NE E)]1046 >lookup_add_miss in H; [ #H @H | @NE ] 1055 1047 ] 1056 1048 ]
Note: See TracChangeset
for help on using the changeset viewer.