Changeset 1244 for src/Clight/CexecComplete.ma

Timestamp:

Sep 21, 2011, 6:08:50 PM (9 years ago)

Author:

campbell

Message:

Sort out Clight semantics equivalence proof for new SmallstepExec?.

File:

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

src/Clight/CexecComplete.ma

@@ -81 +81 @@
 
 theorem the_initial_state:
-  ∀p,s. initial_state p s → ∃ge. yields ? (make_initial_state p) 〈ge,s〉.
-#p #s cases p; #fns #main #globs #H
+  ∀p,s. initial_state p s → yields ? (make_initial_state p) s.
+#p #s cases p; #globs #fns #main #H
 inversion H;
-#b #f #ge #m #e1 #e2 #e3 #e4 #e5 %{ge}
-whd in ⊢ (??%?);
->e1
+#b #f #ge #m #e1 #e2 #e3 #e4 #e5
 whd in ⊢ (??%?);
 >e2
 whd in ⊢ (??%?);
+change in e1:(??%?) with (make_global (mk_program ?? globs fns main))
+>e1
 >e3
 whd in ⊢ (??%?);