From 667a578de4aae51fc75e18d8b97fff13a522b50e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Wed, 3 May 2023 16:29:10 +0200 Subject: [PATCH] Adapt w.r.t. coq/coq#17564. --- src/Instances.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Instances.v b/src/Instances.v index 68366dc17..f0297a159 100644 --- a/src/Instances.v +++ b/src/Instances.v @@ -306,8 +306,8 @@ Proof. { intros. reflexivity. } destruct a. intros _. - destruct H1 as [[_ Hca]]. - destruct H4 as [[_ Hcb]]. + edestruct H1 as [[_ Hca]]. + edestruct H4 as [[_ Hcb]]. destruct Hca as [x1 [s1 [_ Hin1]]]. reflexivity. destruct Hcb as [x2 [s2 [_ Hin2]]]. reflexivity. eexists (x1 + x2). simpl. eexists (s1 + s2). split. reflexivity. @@ -344,7 +344,7 @@ Proof. constructor. split. intros. reflexivity. intros _. simpl. destruct a. - - destruct H as [ [ _ Hc ] ]. destruct Hc as [x [H1 H2]]. reflexivity. + - edestruct H as [ [ _ Hc ] ]. destruct Hc as [x [H1 H2]]. reflexivity. eexists x. split. reflexivity. eapply semOneofSize. eauto with typeclass_instances. eexists. split. right. left.