diff options
Diffstat (limited to 'theories/MSets')
| -rw-r--r-- | theories/MSets/MSetAVL.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v index 5d17dd3f1..db6616b34 100644 --- a/theories/MSets/MSetAVL.v +++ b/theories/MSets/MSetAVL.v @@ -1767,7 +1767,7 @@ Lemma compare_more_Cmp : forall x1 cont x2 r2 e2 l, Cmp (compare_more x1 cont (More x2 r2 e2)) (x1::l) (flatten_e (More x2 r2 e2)). Proof. - simpl; intros; elim_compare x1 x2; simpl; auto. + simpl; intros; elim_compare x1 x2; simpl; red; auto. Qed. Lemma compare_cont_Cmp : forall s1 cont e2 l, |