From fc4f211ec32728f505f4f4375751c1a10278439f Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 12 Apr 2024 00:51:02 +0900 Subject: [PATCH] to please Coq 8.16 --- classical/classical_sets.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/classical/classical_sets.v b/classical/classical_sets.v index fc8742512c..424dcb77e2 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -2690,7 +2690,7 @@ Proof. move=> totP; pose R (sA sB : P) := `[< sval sA `<=` sval sB >]. have {}totR F (FR : total_on F R) : exists sB, forall sA, F sA -> R sA sB. have FP : [set val x | x in F] `<=` P. - by move=> _ [X FX <-]; exact/set_mem/valP. + by move=> _ [X FX <-]; apply: set_mem; exact/valP. have totF : total_on [set val x | x in F] subset. move=> _ _ [X FX <-] [Y FY <-]. by have [/asboolP|/asboolP] := FR _ _ FX FY; [left|right].