diff options
Diffstat (limited to 'theories/Classes/EquivDec.v')
| -rw-r--r-- | theories/Classes/EquivDec.v | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index ff407182d..aa653de0f 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -145,8 +145,3 @@ Program Instance list_eqdec `(eqa : EqDec A eq) : ! EqDec (list A) eq := end }. Solve Obligations using unfold equiv, complement in * ; program_simpl ; intuition (discriminate || eauto). - - Next Obligation. - Proof. clear aux. red in H0. subst. - destruct y; intuition (discriminate || eauto). - Defined. |