Changeset 2222

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:

• ASM/PolicyFront.ma (modified) (1 diff)
• common/Identifiers.ma (modified) (3 diffs)

src/ASM/PolicyFront.ma

@@ -431 +431 @@
     Some ? (pi1 ?? final_policy).
 [ / by I/
-| lapply p -p generalize in match (foldl_strong ?????); * #p #Hp #hg
+| lapply p -p cases final_policy -final_policy #p #Hp #hg
   @conj [ @Hp | @not_lt_to_le @ltb_false_to_not_lt @hg ]
 | @conj [ @conj [ @conj [ @conj

src/common/Identifiers.ma

@@ -809 +809 @@
 [ #_ %
 | #x #l' #Hi
-  whd in match (l'@[x] : identifier_map tag unit);
+  whd in match (set_from_list … (l'@[x]));
   >foldl_append
   #H @All_append
@@ -831 +831 @@
   lapply (All_append_r … H)
   * #Px * #Pl' #i
-  whd in match (l'@[x] : identifier_map ??);
+  whd in match (set_from_list … (l'@[x]));
   >foldl_append
   >mem_set_add
@@ -850 +850 @@
 | #EQ >EQ * #ABS @ABS %
 ] qed.
-
-
-