compatibility with Coq 8.21 and later

[palmskog]

Due to some change in Coq (probably related to cofixpoints) some lemmas with cofix can't get past Qed. By changing have to assert and suff to enough, it works again. Since this concerns ssr_have, it could be related to coq-community/graph-theory#39

Here is a sample of an error on current Coq master that is fixed:

Error:
Recursive definition of dmAR is ill-formed.
In environment
X : Type
R : X -> X -> Prop
P, Q : X -> Prop
R_serial : forall x : X, exists y : X, R x y
xm : XM
w : X
H : ~ cAR R P Q w
C : ~ cEU R (PredC P) (PredC Q) w
dmAR : forall w : X, ~ cEU R (PredC P) (PredC Q) w -> cAR R P Q w
w0 : X
Hw : ~ cEU R (PredC P) (PredC Q) w0
Sub-expression "ssr_have (dn xm (fun H : ~ Q w0 => Hw (EU0 R (PredC P) H)))
                  (fun Qw : Q w0 =>
                   (fun (_evar_0_ : forall a : P w0, (fun=> cAR R P Q w0) (or_introl a))
                      (_evar_0_0 : forall b : ~ P w0, (fun=> cAR R P Q w0) (or_intror b)) =>
                    match xm (P w0) as o return ((fun=> cAR R P Q w0) o) with
                    | or_introl a => _evar_0_ a
                    | or_intror b => _evar_0_0 b
                    end) ((AR0 R (w:=w0))^~ Qw)
                     (fun nPw : ~ P w0 =>
                      ARs Qw
                        (fun (v : X) (wv : R w0 v) =>
                         dmAR v (fun C : cEU R (PredC P) (PredC Q) v => Hw (EUs nPw wv C)))))" not
in guarded form (should be a constructor, an abstraction, a match, a cofix or a recursive
call).
Recursive definition is:
"fun (w : X) (Hw : ~ cEU R (PredC P) (PredC Q) w) =>
 ssr_have (dn xm (fun H : ~ Q w => Hw (EU0 R (PredC P) H)))
   (fun Qw : Q w =>
    (fun (_evar_0_ : forall a : P w, (fun=> cAR R P Q w) (or_introl a))
       (_evar_0_0 : forall b : ~ P w, (fun=> cAR R P Q w) (or_intror b)) =>
     match xm (P w) as o return ((fun=> cAR R P Q w) o) with
     | or_introl a => _evar_0_ a
     | or_intror b => _evar_0_0 b
     end) ((AR0 R (w:=w))^~ Qw)
      (fun nPw : ~ P w =>
       ARs Qw
         (fun (v : X) (wv : R w v) =>
          dmAR v (fun C : cEU R (PredC P) (PredC Q) v => Hw (EUs nPw wv C)))))".

and here is what the correct body looks like with assert:

fun (xm : XM) (w : X) (H : ~ cAR R P Q w) =>
dn xm
  (fun C : ~ cEU R (PredC P) (PredC Q) w =>
   H
     ((cofix dmAR (w0 : X) (Hw : ~ cEU R (PredC P) (PredC Q) w0) : cAR R P Q w0 :=
         let Qw : Q w0 := dn xm (fun H0 : ~ Q w0 => Hw (EU0 R (PredC P) H0)) in
         (fun (_evar_0_ : forall a : P w0, (fun=> cAR R P Q w0) (or_introl a))
            (_evar_0_0 : forall b : ~ P w0, (fun=> cAR R P Q w0) (or_intror b)) =>
          match xm (P w0) as o return ((fun=> cAR R P Q w0) o) with
          | or_introl a => _evar_0_ a
          | or_intror b => _evar_0_0 b
          end) ((AR0 R (w:=w0))^~ Qw)
           (fun nPw : ~ P w0 =>
            ARs Qw
              (fun (v : X) (wv : R w0 v) =>
               dmAR v (fun C0 : cEU R (PredC P) (PredC Q) v => Hw (EUs nPw wv C0))))) w C))
     : XM -> forall [w : X], ~ cAR R P Q w -> cEU R (PredC P) (PredC Q) w

[palmskog]

@chdoc do you think we should merge this or wait hear first from MathComp/Coq devs? Mixing have/assert is obviously unidiomatic...

[palmskog]

Confirmed this was related to changes in opacity and thus coq-community/graph-theory#39 and managed to get away with only have @ (but had to drop suff), so I think it's now sufficiently idiomatic to merge.