Ignore:
Timestamp:
Jan 25, 2011, 5:30:36 PM (9 years ago)
Author:
campbell
Message:

Prevent clashes between names in AST and other parts of the development.
(Noticed when trying a large example file.)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Csem.ma

    r474 r478  
    14811481  without arguments and with an empty continuation. *)
    14821482
    1483 ninductive initial_state (p: program): state -> Prop :=
     1483ninductive initial_state (p: clight_program): state -> Prop :=
    14841484  | initial_state_intro: ∀b,f.
    14851485      let ge := globalenv Genv ?? p in
     
    15001500  behavior. *)
    15011501
    1502 ndefinition exec_program : program → program_behavior → Prop ≝ λp,beh.
     1502ndefinition exec_program : clight_program → program_behavior → Prop ≝ λp,beh.
    15031503  program_behaves (mk_transrel ?? step) (initial_state p) final_state (globalenv ??? p) beh.
    15041504(*
Note: See TracChangeset for help on using the changeset viewer.