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.