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 9c600b01e..9f44d4fef 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -141,5 +141,5 @@ Program Instance list_eqdec `(eqa : EqDec A eq) : ! EqDec (list A) eq := Next Obligation. destruct y ; intuition eauto. Defined. - Solve Obligations using unfold equiv, complement in * ; + Solve Obligations with unfold equiv, complement in * ; program_simpl ; intuition (discriminate || eauto). |