With Coq PR #13513, "intros []" uses "destruct" rather than "case" and becomes "smarter".
requested to merge herbelin/flocq:master+adapt-coq-pr13513-disjunctive-intro-pattern-is-destruct into master
As a consequence, a clear becomes useless.
We leave a try so as to be backwards-compatible.