From 967ab62267722819dab1b3dfea1805b060daada3 Mon Sep 17 00:00:00 2001
From: Jonathan Chan <jonathanhwchan@gmail.com>
Date: Tue, 18 Apr 2023 16:19:27 -0400
Subject: [PATCH] Fix universe inconsistency issue.

---
 theories/Eq/SSim.v           | 2 +-
 theories/Interp/FoldCTree.v  | 9 +++------
 theories/Logic/ctl_yannick.v | 2 +-
 3 files changed, 5 insertions(+), 8 deletions(-)

diff --git a/theories/Eq/SSim.v b/theories/Eq/SSim.v
index c647c86..964d094 100644
--- a/theories/Eq/SSim.v
+++ b/theories/Eq/SSim.v
@@ -1047,7 +1047,7 @@ Section Proof_Rules.
     With invisible schedules, they are always equivalent: neither of them
     produce any challenge for the other.
 |*)
-  Lemma spinS_gen_nonempty : forall {Z Y D F} {L: rel (label E) (label F)} `{HasStuck': B0 -< D}
+  Lemma spinS_gen_nonempty : forall {Z X Y D F} {L: rel (label E) (label F)} `{HasStuck': B0 -< D}
                                (c: C X) (c': C Y) (x: X) (y: Y),
       L tau tau ->
       ssim L (@spinS_gen E C Z X c) (@spinS_gen F C Z Y c').
diff --git a/theories/Interp/FoldCTree.v b/theories/Interp/FoldCTree.v
index ff00ae8..2aeeb9f 100644
--- a/theories/Interp/FoldCTree.v
+++ b/theories/Interp/FoldCTree.v
@@ -26,7 +26,6 @@ Open Scope ctree_scope.
     For now, we simply specialize results to specific [M]s.
  *)
 
-Unset Universe Checking.
 Theorem ssim_interp_h {E F1 F2 C D1 D2 X Y}
   `{HasB0 : B0 -< D1} `{HasB1 : B1 -< D1} `{HasB0' : B0 -< D2} `{HasB1' : B1 -< D2}
   `{HC1 : C -< D1} `{HC2 : C -< D2}
@@ -47,9 +46,8 @@ Proof.
     apply equ_vis_invT in H1 as ?. subst.
     eapply ssim_clo_bind_gen with (R0 := eq).
     + red. reflexivity.
-    + admit. (* FIXME universe inconsistency *)
-      (*eapply weq_ssim. apply update_val_rel_update_val_rel.
-      apply equ_vis_invE in H1 as [<- ?]. apply H0.*)
+    + eapply weq_ssim. apply update_val_rel_update_val_rel.
+      apply equ_vis_invE in H1 as [<- ?]. apply H0.
     + intros. step. apply step_ss_ret. constructor.
       apply equ_vis_invE in H1 as [<- ?]. subst. apply H1.
   - unfold CTree.map. setoid_rewrite bind_branch.
@@ -58,8 +56,7 @@ Proof.
     destruct vis.
     + step. apply step_ss_brS. intros. exists x0. step. apply step_ss_ret. constructor. apply H1. right; auto. 3: apply H. all: intros H2; inversion H2.
     + step. apply step_ss_brD. intros. exists x0. apply step_ss_ret. constructor. apply H1.
-Admitted.
-Set Universe Checking.
+Qed.
 
 Section FoldCTree.
 
diff --git a/theories/Logic/ctl_yannick.v b/theories/Logic/ctl_yannick.v
index ca12755..001ae87 100644
--- a/theories/Logic/ctl_yannick.v
+++ b/theories/Logic/ctl_yannick.v
@@ -732,7 +732,7 @@ Module Termination.
     econstructor.
 Qed.
 
-End Termination
+End Termination.
  
                   
 Module Scheduling.