diff options
| -rw-r--r-- | theories/Classes/EquivDec.v | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index 6978fa1ddf..a1a4da6f37 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -87,7 +87,7 @@ Program Instance unit_eqdec : EqDec unit eq := fun x y => in_left. Next Obligation. Proof. - destruct x ; destruct y. + do 2 match goal with [ x : () |- _ ] => destruct x end. reflexivity. Qed. @@ -142,7 +142,10 @@ Program Instance list_eqdec `(eqa : EqDec A eq) : EqDec (list A) eq := | _, _ => in_right end }. - Next Obligation. destruct y ; unfold not in *; eauto. Defined. + Next Obligation. + match goal with y : list _ |- _ => destruct y end ; + unfold not in *; eauto. + Defined. Solve Obligations with unfold equiv, complement in * ; program_simpl ; intuition (discriminate || eauto). |