From f365b8f62b4de5f3d72a67f04668d00d7ed95b6e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 10 Jun 2026 15:48:53 +0200 Subject: [PATCH] More accurate clears after proof using --- utils/theories/wGraph.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/utils/theories/wGraph.v b/utils/theories/wGraph.v index 8c8232f83..e538c01a1 100644 --- a/utils/theories/wGraph.v +++ b/utils/theories/wGraph.v @@ -1970,7 +1970,7 @@ Module WeightedGraph (V : UsualOrderedType) (VSet : MSetInterface.S with Module | inr (q1, q2) => weight q1 + K + weight q2 end. Proof using HI Hxs. - clear -HI HG Hxs. + clear -HI Hxs. induction q. - reflexivity. - simpl. @@ -2019,7 +2019,7 @@ Module WeightedGraph (V : UsualOrderedType) (VSet : MSetInterface.S with Module | inr (q1, q2) => sweight q1 + K + sweight q2 end. Proof using HI Hxs. - clear -HI HG Hxs. + clear -HI Hxs. induction q. - reflexivity. - simpl.