Ignore:
Timestamp:
Jun 21, 2012, 5:21:02 PM (9 years ago)
Author:
campbell
Message:

Make transform_*program take a more general transformation to make
properties easier to state.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/labelSimulation.ma

    r2050 r2103  
    1818(* FIXME with a more general result *)
    1919axiom transform_program_related : ∀F,V,init,t,p.
    20   related_globals F t (globalenv (λ_.F) V init p) (globalenv (λ_.F) V init (transform_program … p t)).
     20  related_globals F t (globalenv (λ_.F) V init p) (globalenv (λ_.F) V init (transform_program … p (λ_.t))).
    2121(*
    2222#F #V #init #t * #vars #fns #main
     
    11141114% [2: %
    11151115[ whd in ⊢ (??%?);
    1116   change with (transform_program ??? (mk_program …) label_fundef) in match (mk_program ??? (transf_program ????) ?);
     1116  change with (transform_program ??? (mk_program …) (λ_.label_fundef)) in match (mk_program ??? (transf_program ????) ?);
    11171117  <transform_program_init_mem >Em in ⊢ (??%?);
    11181118  whd in ⊢ (??%?); <(rg_find_symbol … RG) >Emain in ⊢ (??%?);
Note: See TracChangeset for help on using the changeset viewer.