Changeset 2680 for src


Ignore:
Timestamp:
Feb 19, 2013, 4:36:52 PM (7 years ago)
Author:
mckinna
Message:

proofs which previously succeeded fail, thanks to fold on positive_map no longer unfolding (enough); marked with XXX
Correction: do more normalisation/conversion explicitly
Real solution: idnetify what's changed to expose this fragility (in normalisation?)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/switchRemoval.ma

    r2677 r2680  
    943943     whd in match (fold ?????) in ⊢ (??%%);
    944944     cases optblock
    945      [ 1: normalize nodelta >Hind1 >Hind2 >Hind2 in ⊢ (???%);
     945     [ 1: normalize (* XXX nodelta not enough here *) >Hind1 >Hind2 >Hind2 in ⊢ (???%);
    946946          >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 ⊢ (???%);
    948948          >Hind1 in ⊢ (???%); >append_cons <associative_append @refl
    949949     ]
     
    986986          whd in match (lookup_opt ???);
    987987          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)
    989991          | 2: #p #Hright lapply (Hind2 … Hright)
    990992                normalize >fold_to_concat in ⊢ (? → %);
Note: See TracChangeset for help on using the changeset viewer.