diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Classes/SetoidDec.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index 2947c4831f..f4220e3aa1 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -96,7 +96,7 @@ Program Instance unit_eqdec : EqDec (eq_setoid unit) := Next Obligation. Proof. - destruct x ; destruct y. + do 2 match goal with x : () |- _ => destruct x end. reflexivity. Qed. |