diff --git a/theories/spanning_tree/mon.v b/theories/spanning_tree/mon.v index fd68ebcdde227f551c987dd10db806861798acc1..615df852b7816cb64c4ece73b341d7dc7626dd48 100644 --- a/theories/spanning_tree/mon.v +++ b/theories/spanning_tree/mon.v @@ -70,7 +70,7 @@ Definition Gmon := gmapR loc (exclR chlO). Definition excl_chlC_chl (ch : exclR chlO) : option (option loc * option loc) := match ch with | Excl w => Some w - | ExclBot => None + | ExclInvalid => None end. Definition Gmon_graph (G : Gmon) : graph loc := omap excl_chlC_chl G.