From 10ed87199a833c06c3f857dafd2d7e23b0c900ab Mon Sep 17 00:00:00 2001 From: Jonas Kastberg Hinrichsen <jihgfee@gmail.com> Date: Thu, 27 Feb 2025 12:50:09 +0100 Subject: [PATCH] Bump stdpp --- actris/examples/map_reduce.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/actris/examples/map_reduce.v b/actris/examples/map_reduce.v index 479401b..5da7132 100644 --- a/actris/examples/map_reduce.v +++ b/actris/examples/map_reduce.v @@ -211,7 +211,7 @@ Section mapper. inversion 1 as [|?? [? _]]; discriminate_list || simplify_list_eq. assert (RZB (j',y') (i,y'')) as [??]; last (simpl in *; lia). apply (Sorted_StronglySorted _) in Hsort. - eapply elem_of_StronglySorted_app; set_solver. + eapply StronglySorted_app; set_solver. Qed. Lemma par_map_reduce_reduce_spec n iys iys_sorted miy zs l Y csort cred : -- GitLab