Changeset 2686 for src


Ignore:
Timestamp:
Feb 21, 2013, 3:34:29 PM (7 years ago)
Author:
mckinna
Message:

two minor modifications to assist disambiguation of "lookup"

file still sensitive to disambiguation (errors/failures) in ASM/Arithmetic.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r2645 r2686  
    10591059    whd in ⊢ (% → %);
    10601060    whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?);
    1061     cases (lookup ??? id)
     1061    cases (lookup ?? (add_tmps …) id)
    10621062    [ * | #x #_ % #E destruct ]
    10631063  ]
     
    10911091>lookup_add_miss // @(fresh_distinct … E1) @F1
    10921092whd in H:(match % with [_ ⇒ ?|_ ⇒ ?]) ⊢ %;
    1093 cases (lookup ??? id) in H ⊢ %;
     1093cases (lookup ?? (add_tmps …) id) in H ⊢ %;
    10941094[ * | #x #_ % #E destruct ]
    10951095qed.
Note: See TracChangeset for help on using the changeset viewer.