Changeset 1228


Ignore:
Timestamp:
Sep 19, 2011, 4:52:40 PM (8 years ago)
Author:
mulligan
Message:

some more changes

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/build.ma

    r1227 r1228  
    11include "ERTL/liveness.ma".
    2 include "utilities/Interference.ma".
     2(* include "utilities/Interference.ma". *)
    33
    44definition vertex ≝ register ⊎ Register.
     
    99}.
    1010
    11 axiom create: ∀globals: list ident. ertl_internal_function globals → graph.
     11axiom build: ∀globals: list ident. ertl_internal_function globals → graph.
    1212
    1313inductive decision: Type[0] ≝
  • src/joint/Joint.ma

    r1220 r1228  
    8383definition joint_function ≝ λglobals,pre,p. fundef (joint_internal_function globals pre p).
    8484
    85 definition joint_program :=
    86  λglobals:list ident.λpre.λp: sem_params_ pre globals.
    87   program (joint_function … p) nat.
     85definition joint_program ≝
     86  λglobals: list ident.
     87  λpre.
     88  λp: sem_params_ pre globals.
     89    program (λx. joint_function globals pre p) nat.
    8890
    8991(****************************************************************************)
Note: See TracChangeset for help on using the changeset viewer.