Commit 82d3fc4f authored by Ralf Jung's avatar Ralf Jung

use naive_solver instead of firstorder

parent dd8bcd0f
Pipeline #25461 canceled with stage
in 6 minutes and 56 seconds
......@@ -1015,7 +1015,7 @@ Section Progress.
destruct (NUB _ _ IN PLN) as [v0 [REL Comp0]].
inversion REL; subst; [|by inversion Comp0].
eapply CasFailS; [eauto..| |done]. rewrite H1 in H0. inversion H0. subst.
inversion Comp0; subst; constructor; clear -NEQ; firstorder.
inversion Comp0; subst; constructor; clear -NEQ; naive_solver.
+ clear READ DRFP NEQ NUB.
move => evt2 e2 efs2 ots 𝑚s2 𝓥2 M2 𝓢2 STEP' MSTEP'. inversion STEP'.
* subst. simplify_eq. constructor. clear - DRFR RLXR.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment