From eede8c539985e358e7149ab77b5c058def37571d Mon Sep 17 00:00:00 2001 From: Li-yao Xia Date: Thu, 18 May 2023 15:49:43 +0100 Subject: [PATCH] Fix FailFacts for coq-dev --- theories/Events/FailFacts.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/theories/Events/FailFacts.v b/theories/Events/FailFacts.v index 2b1f506e..3ed9a608 100644 --- a/theories/Events/FailFacts.v +++ b/theories/Events/FailFacts.v @@ -102,9 +102,9 @@ Section FailTLaws. + rewrite bind_ret_l; reflexivity. - repeat intro; cbn. eapply eutt_clo_bind; eauto. - intros [] [] REL; cbn in *; subst; try intuition discriminate. - rewrite H0; reflexivity. - reflexivity. + intros [] [] REL; cbn in *; subst; try contradiction. + + apply H0. + + reflexivity. Qed. End FailTLaws.