Modify Classes/EquivDec.v to compile with -mangle-names

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).