diff options
| -rw-r--r-- | theories/Classes/EquivDec.v | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index fd8576a8cd..17f8970fc9 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -132,7 +132,6 @@ Program Instance [ EqDec A eq ] => bool_function_eqdec : ! EqDec (bool -> A) eq Next Obligation. Proof. - red. extensionality x. destruct x ; auto. Qed. |