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
5 files
+ 23
− 16
Compare changes
  • Side-by-side
  • Inline
Files
5
theories/typing/fixpoint.v
+ 1
− 1
@@ -12,7 +12,7 @@ Section fixpoint_def.
@@ -12,7 +12,7 @@ Section fixpoint_def.
Local Instance type_2_contractive : Contractive (Nat.iter 2 T).
Local Instance type_2_contractive : Contractive (Nat.iter 2 T).
Proof using Type*.
Proof using Type*.
intros n ? **. simpl.
intros n ? **. simpl.
by apply dist_later_dist, type_dist2_dist_later, HT, HT, type_later_dist2_later.
by apply dist_later_S, type_dist2_dist_later, HT, HT, type_later_dist2_later.
Qed.
Qed.
Definition type_fixpoint : type := fixpointK 2 T.
Definition type_fixpoint : type := fixpointK 2 T.