Changeset 2682 for src/Clight/labelSimulation.ma

Timestamp:

Feb 19, 2013, 7:24:20 PM (7 years ago)

Author:

campbell

Message:

Don't apply inv in after_n_steps to last state.

File:

• src/Clight/labelSimulation.ma (modified) (1 diff)

src/Clight/labelSimulation.ma

@@ -1021 +1021 @@
     >shift_fst whd in match (seq_of_labeled_statement ?);
     cases (step_with_labels_partial … RG (State f s k e m) (State (\fst (label_function u0 f)) (\fst (label_statement s u)) k' e m) tr s2 (swl_state … K) EX)
-    #n #H %{(S n)} @(after_n_m 1 (S n) … H) % /2/
+    #n #H %{(S n)} @(after_n_m 1 (S n) … H) // % /2/
     #trx #sx * /3/
 (* but for LScase it's just like the cases in step_with_labels_partial *)