PrincetonUniversity / VST

Verified Software Toolchain
https://vst.cs.princeton.edu
Other
436 stars 92 forks source link

Small concurrency fixes #617

Closed andrew-appel closed 2 years ago

andrew-appel commented 2 years ago
  1. Removed an unnecessary premise from data_at_rec_share_join_values_cohere
  2. added atomics/verif_lock.vo to make target "simpleconc" and therefore to target "vst"
  3. fixed a bug in Ltac forward_spawn