From 05eb175eaac893a2c8c70b088b8f93b97af06919 Mon Sep 17 00:00:00 2001
From: Johannes Kloos <jkloos@mpi-sws.org>
Date: Thu, 9 Nov 2017 22:18:15 +0100
Subject: [PATCH] Fix the size of wg_guard unfolding
---
theories/infinite.v | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
diff --git a/theories/infinite.v b/theories/infinite.v
index 23767b8..9e4488c 100644
--- a/theories/infinite.v
+++ b/theories/infinite.v
@@ -71,7 +71,7 @@ Section Fresh.
apply inbelow; omega.
Qed.
- Instance fresh_generic: Fresh A C := λ s, fresh_generic_fix s 0.
+ Instance fresh_generic: Fresh A C := λ s, fresh_generic_fix 20 s 0.
Instance fresh_generic_spec: FreshSpec A C.
Proof.
@@ -79,16 +79,16 @@ Section Fresh.
- apply _.
- intros * eqXY.
unfold fresh, fresh_generic.
- destruct (fresh_generic_fixpoint_spec (1 + Nat.log2 (size X)) X 0)
+ destruct (fresh_generic_fixpoint_spec 20 X 0)
as [mX [_ [-> [notinX belowinX]]]].
- destruct (fresh_generic_fixpoint_spec (1 + Nat.log2 (size Y)) Y 0)
+ destruct (fresh_generic_fixpoint_spec 20 Y 0)
as [mY [_ [-> [notinY belowinY]]]].
destruct (Nat.lt_trichotomy mX mY) as [case|[->|case]]; auto.
+ contradict notinX; rewrite eqXY; apply belowinY; omega.
+ contradict notinY; rewrite <- eqXY; apply belowinX; omega.
- intro.
unfold fresh, fresh_generic.
- destruct (fresh_generic_fixpoint_spec (1 + Nat.log2 (size X)) X 0)
+ destruct (fresh_generic_fixpoint_spec 20 X 0)
as [m [_ [-> [notinX belowinX]]]]; auto.
Qed.
End Fresh.
--
GitLab