Ignore:
Timestamp:
Apr 9, 2012, 3:07:06 PM (8 years ago)
Author:
campbell
Message:

Syntax changes to fit Paolo's commit.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r1878 r1884  
    122122    let 〈c,stack_high〉 ≝
    123123      (* if the (local, parameter) variable is of a compound type OR if its adress is taken, we allocate it on the stack. *)
    124       if always_alloc ty ∨ mem_set ? mem_vars id then
     124      if always_alloc ty ∨ id ∈ mem_vars then
    125125        〈Stack stack_high,stack_high + sizeof ty〉
    126126      else
     
    177177  #H >(contract_pair var_types nat ?) in E;
    178178  whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
    179   cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
     179  cases (always_alloc ty ∨ id ∈ ?) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
    180180  #H' lapply (extract_pair ???????? H') -H' * #m0 * #n0 * #EQ #EQ2
    181181  cases (identifier_eq ? i id)
     
    212212  #H >(contract_pair var_types nat ?) in E;
    213213  whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
    214   cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
     214  cases (always_alloc ty ∨ id ∈ ?) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
    215215  #H' lapply (extract_pair ???????? H') -H' * #m0 * #n0 * #EQ #EQ2
    216216
Note: See TracChangeset for help on using the changeset viewer.