Changeset 1629 for src/Clight/fresh.ma


Ignore:
Timestamp:
Dec 19, 2011, 2:48:35 PM (8 years ago)
Author:
campbell
Message:

Sort out most of the fresh names stuff in Clight to Cminor.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/fresh.ma

    r1628 r1629  
    77
    88include "Clight/Csyntax.ma".
     9include "utilities/lists.ma".
    910
    1011definition max_id : ident → ident → ident ≝
     
    5960  ].
    6061
     62definition globals_fresh_for_univ : ∀V:Type[0]. list (ident × region × V) → universe SymbolTag → Prop ≝
     63λV,gl,u.  All ? (λv. fresh_for_univ ? (\fst (\fst v)) u) gl.
     64
    6165definition prog_fresh_for_univ : clight_program → universe SymbolTag → Prop ≝
    6266λp,u.
    6367  All ? (λifd. fresh_for_univ ? (\fst ifd) u ∧ fd_fresh_for_univ (\snd ifd) u) (prog_funct ?? p) ∧
    6468  fresh_for_univ ? (prog_main ?? p) u ∧
    65   All ? (λv. fresh_for_univ ? (\fst (\fst v)) u) (prog_vars ?? p).
     69  globals_fresh_for_univ ? (prog_vars ?? p) u.
    6670
    6771(* And they match up. *)
Note: See TracChangeset for help on using the changeset viewer.