Skip to content
Snippets Groups Projects

fix for iris!886 and iris!896

Merged fix for iris!886 and iris!896
msammler/new_contractive into master
All threads resolved!
Merged Michael Sammler requested to merge msammler/new_contractive into master
All threads resolved!
Compare
and
17 files
+ 37
− 36
Compare changes
  • Side-by-side
  • Inline
Files
17
theories/typing/lib/mutex/mutex.v
+ 1
− 1
@@ -79,7 +79,7 @@ Section mutex.
@@ -79,7 +79,7 @@ Section mutex.
Proof.
Proof.
constructor;
constructor;
solve_proper_core ltac:(fun _ => exact: type_dist2_S ||
solve_proper_core ltac:(fun _ => exact: type_dist2_S ||
f_type_equiv || f_contractive || f_equiv).
f_type_equiv || f_contractive_fin || f_equiv).
Qed.
Qed.
Global Instance mutex_ne : NonExpansive mutex.
Global Instance mutex_ne : NonExpansive mutex.