diff options
Diffstat (limited to 'theories/Classes/EquivDec.v')
| -rw-r--r-- | theories/Classes/EquivDec.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index 9f44d4fef..87f86e0d3 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -139,7 +139,7 @@ Program Instance list_eqdec `(eqa : EqDec A eq) : ! EqDec (list A) eq := | _, _ => in_right end }. - Next Obligation. destruct y ; intuition eauto. Defined. + Next Obligation. destruct y ; unfold not in *; eauto. Defined. Solve Obligations with unfold equiv, complement in * ; program_simpl ; intuition (discriminate || eauto). |