Clean a paren pair

mit-plv · Aug 10, 2024 · bac5f89 · bac5f89
1 parent f8e4b66
commit bac5f89
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/LiveVerif/src/LiveVerifExamples/critbit.v b/LiveVerif/src/LiveVerifExamples/critbit.v
@@ -2751,7 +2751,7 @@ Derive critical_bit SuchThat (fun_correct! critical_bit) As critical_bit_ok.
   move i at bottom. .**/
   while (i < 8 * sizeof(uintptr_t) - 1
     && ((k1 >> (8 * sizeof(uintptr_t) - 1 - i) & 1)
-          == ((k2 >> (8 * sizeof(uintptr_t) - 1 - i) & 1))))
+          == (k2 >> (8 * sizeof(uintptr_t) - 1 - i) & 1)))
     /* decreases (ltac:(bw) - \[i]) */ {                                   /**. .**/
     i = i + 1;                                                             /**. .**/
   }                                                                        /**.