Changeset 2222


Ignore:
Timestamp:
Jul 20, 2012, 10:58:15 AM (7 years ago)
Author:
sacerdot
Message:

More robust to possible future changes to the "in match" semantics
(that would be weakened).

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyFront.ma

    r2221 r2222  
    431431    Some ? (pi1 ?? final_policy).
    432432[ / by I/
    433 | lapply p -p generalize in match (foldl_strong ?????); * #p #Hp #hg
     433| lapply p -p cases final_policy -final_policy #p #Hp #hg
    434434  @conj [ @Hp | @not_lt_to_le @ltb_false_to_not_lt @hg ]
    435435| @conj [ @conj [ @conj [ @conj
  • src/common/Identifiers.ma

    r2182 r2222  
    809809[ #_ %
    810810| #x #l' #Hi
    811   whd in match (l'@[x] : identifier_map tag unit);
     811  whd in match (set_from_list … (l'@[x]));
    812812  >foldl_append
    813813  #H @All_append
     
    831831  lapply (All_append_r … H)
    832832  * #Px * #Pl' #i
    833   whd in match (l'@[x] : identifier_map ??);
     833  whd in match (set_from_list … (l'@[x]));
    834834  >foldl_append
    835835  >mem_set_add
     
    850850| #EQ >EQ * #ABS @ABS %
    851851] qed.
    852 
    853 
    854 
Note: See TracChangeset for help on using the changeset viewer.