Changeset 725 for src/Clight/Csem.ma


Ignore:
Timestamp:
Mar 30, 2011, 4:16:08 PM (9 years ago)
Author:
campbell
Message:

Do some light manual disambiguation to make Clight examples go through more
easily.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csem.ma

    r717 r725  
    452452  and function pointers to their definitions.  (See module [Globalenvs].) *)
    453453
    454 definition genv ≝ (genv_t Genv) fundef.
     454definition genv ≝ (genv_t Genv) clight_fundef.
    455455
    456456(* * The local environment maps local variables to block references.
     
    924924      ∀m: mem.  state
    925925  | Callstate:
    926       ∀fd: fundef.
     926      ∀fd: clight_fundef.
    927927      ∀args: list val.
    928928      ∀k: cont.
     
    11521152      alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) e m1 →
    11531153      bind_parameters e m1 (fn_params f) vargs m2 →
    1154       step ge (Callstate (Internal f) vargs k m)
     1154      step ge (Callstate (CL_Internal f) vargs k m)
    11551155           E0 (State f (fn_body f) k e m2)
    11561156
    11571157  | step_external_function: ∀id,targs,tres,vargs,k,m,vres,t.
    11581158      event_match (external_function id targs tres) vargs t vres →
    1159       step ge (Callstate (External id targs tres) vargs k m)
     1159      step ge (Callstate (CL_External id targs tres) vargs k m)
    11601160            t (Returnstate vres k m)
    11611161
Note: See TracChangeset for help on using the changeset viewer.