diff options
Diffstat (limited to 'theories/Classes')
| -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 bafbac3f1f..0a35ef45e0 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -130,7 +130,7 @@ Require Import List. Program Instance list_eqdec `(eqa : EqDec A eq) : ! EqDec (list A) eq := { equiv_dec := - fix aux (x : list A) y { struct x } := + fix aux (x y : list A) := match x, y with | nil, nil => in_left | cons hd tl, cons hd' tl' => |