Changeset 2680 for src/Clight/switchRemoval.ma
- Timestamp:
- Feb 19, 2013, 4:36:52 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/switchRemoval.ma
r2677 r2680 943 943 whd in match (fold ?????) in ⊢ (??%%); 944 944 cases optblock 945 [ 1: normalize nodelta>Hind1 >Hind2 >Hind2 in ⊢ (???%);945 [ 1: normalize (* XXX nodelta not enough here *) >Hind1 >Hind2 >Hind2 in ⊢ (???%); 946 946 >associative_append @refl 947 | 2: #block normalize nodelta>Hind1 >Hind2 >Hind2 in ⊢ (???%);947 | 2: #block normalize (* XXX nodelta not enough here *) >Hind1 >Hind2 >Hind2 in ⊢ (???%); 948 948 >Hind1 in ⊢ (???%); >append_cons <associative_append @refl 949 949 ] … … 986 986 whd in match (lookup_opt ???); 987 987 cases id normalize nodelta 988 [ 1: #Habsurd destruct (Habsurd) 988 [ 1: #Habsurd 989 (* XXX nodelta not enough here *) change with (None ? = Some …) in Habsurd; 990 destruct (Habsurd) 989 991 | 2: #p #Hright lapply (Hind2 … Hright) 990 992 normalize >fold_to_concat in ⊢ (? → %);
Note: See TracChangeset
for help on using the changeset viewer.