fix adequacy

e96df13c · Michael Sammler · 92b01682 · e96df13c
Commit e96df13c authored Nov 10, 2020 by Michael Sammler
Hide whitespace changes
Inline Side-by-side

Showing with 2 additions and 1 deletion

tutorial/adequacy/adequacy.v tutorial/adequacy/adequacy.v +2 -1

No files found.
--- a/tutorial/adequacy/adequacy.v
+++ b/tutorial/adequacy/adequacy.v
 From refinedc.typing Require Import typing.
 From refinedc.examples.spinlock Require Import
-  generated_code spinlock_def spinlock_proof.
+  generated_code spinlock_def spinlock_proof
+  generated_proof_sl_lock generated_proof_sl_unlock.
 From refinedc.examples.latch Require Import
  generated_code latch_def generated_proof_latch_release
  generated_proof_latch_wait.