Changeset 1610

Timestamp:

Dec 14, 2011, 3:33:57 PM (8 years ago)

Author:

sacerdot

Message:

Ported to new lib.

File:

• src/Cminor/initialisation.ma (modified) (2 diffs)

src/Cminor/initialisation.ma

@@ -53 +53 @@
 | elim init
   [ % //
-  | #h #t #IH whd in ⊢ (?(???%)); @breakup_pair whd in ⊢ (?%); % [ % [ % // | @(pi2 ? stmt_inv) ] | @IH ]
+  | #h #t #IH whd in ⊢ (?(???%)); @breakup_pair whd in ⊢ (?%); % [ % [ % // | @(pi2 … (init_datum …)) ] | @IH ]
 ] qed. 
 
 definition init_vars : list (ident × region × (list init_data)) → Σs:stmt. stmt_inv s ≝
 λvars. foldr ? (Σs:stmt. stmt_inv s)
-  (λvar,s. dp ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst var)) (\snd (\fst var)) (\snd var))) ?) (dp ? (λx.stmt_inv x ) St_skip (conj ?? I I)) vars.
-% [ % [ % // | @(pi2 ? stmt_inv) ] | @(pi2 ? stmt_inv) ]
+  (λvar,s. mk_Sig ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst var)) (\snd (\fst var)) (\snd var))) ?) (mk_Sig ? (λx.stmt_inv x ) St_skip (conj ?? I I)) vars.
+% [ % [ % // | @(pi2 … s) ] | @(pi2 … (init_var …)) ]
 qed.
 
@@ -77 +77 @@
                               list (ident × (fundef internal_function)) →
                               list (ident × (fundef internal_function)) ≝
-λid,s. match s with [ dp s H ⇒
+λid,s. match s with [ mk_Sig s H ⇒
   map ??
     (λidf.