Fix FailFacts for coq-dev

DeepSpec · May 18, 2023 · eede8c5 · eede8c5
1 parent 8e28e2e
commit eede8c5
Showing 1 changed file with 3 additions and 3 deletions.
diff --git 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.