Changeset 2222 for src/common


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).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.