New version of des* works incorrectly in presence of section hypotheses w/ conjunction

[anlun]

From hahn Require Import Hahn.

Section aa.
  Variables A B C D : Prop.

  Hypothesis HH : A /\ B.

  Lemma aaa (OO : C \/ D) : False.
  Proof.
    desf.
  Admitted.
End aa.

In the code above, desf doesn't destruct OO. However, if you put clear HH before desf, then it does.