Changeset 2653 for src

Timestamp:

Feb 8, 2013, 1:45:22 PM (8 years ago)

Author:

sacerdot

Message:

...

Location:

src/ASM

Files:

• Policy.ma (modified) (1 diff)
• PolicyFront.ma (modified) (1 diff)

src/ASM/Policy.ma

@@ -199 +199 @@
    | #Heq lapply (refl ? (jump_expansion_internal program (S (S n))))
      whd in match (jump_expansion_internal program (S (S n))) in ⊢ (???% → ?); >Seq
-     normalize nodelta #Teq >Teq -Teq cases (jump_expansion_step program ??) in Heq Seq; (*320s*)
+     normalize nodelta #Teq >Teq -Teq cases (jump_expansion_step program ??) in Heq Seq ⊢ ?; (*320s*)
      #x cases x -x #Sno_ch #Spol normalize nodelta cases Spol
      [ normalize nodelta #HSn #Heq #Seq cases Heq

src/ASM/PolicyFront.ma

@@ -202 +202 @@
  λold_sigma:ppc_pc_map.λsigma:ppc_pc_map.
  ∀i.i < |prefix| →
- let 〈label,instr〉 ≝ nth i ? prefix 〈None ?, Comment [ ]〉 in
+ let 〈label,instr〉 ≝ nth i ? prefix 〈None ?, Comment EmptyString〉 in
  ∀dest.is_jump_to instr dest → 
  let paddr ≝ lookup_def … labels dest 0 in