Changeset 2680 for src/Clight/switchRemoval.ma

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:

• src/Clight/switchRemoval.ma (modified) (2 diffs)

src/Clight/switchRemoval.ma

@@ -943 +943 @@
      whd in match (fold ?????) in ⊢ (??%%);
      cases optblock
-     [ 1: normalize nodelta >Hind1 >Hind2 >Hind2 in ⊢ (???%);
+     [ 1: normalize (* XXX nodelta not enough here *) >Hind1 >Hind2 >Hind2 in ⊢ (???%);
           >associative_append @refl
-     | 2: #block normalize nodelta >Hind1 >Hind2 >Hind2 in ⊢ (???%);
+     | 2: #block normalize (* XXX nodelta not enough here *) >Hind1 >Hind2 >Hind2 in ⊢ (???%);
           >Hind1 in ⊢ (???%); >append_cons <associative_append @refl
      ]
@@ -986 +986 @@
           whd in match (lookup_opt ???);
           cases id normalize nodelta
-          [ 1: #Habsurd destruct (Habsurd)
+          [ 1: #Habsurd 
+             (* XXX nodelta not enough here *) change with (None ? = Some …) in Habsurd; 
+                destruct (Habsurd)
           | 2: #p #Hright lapply (Hind2 … Hright)
                 normalize >fold_to_concat in ⊢ (? → %);