Unset Asymmetric Patterns

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16129 85f007b7-540e-0410-9357-904b9bb8a0f7

8 files changed, 49 insertions, 29 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/1834.v b/test-suite/bugs/closed/shouldsucceed/1834.v
index 947d15f0d2..884ac01cd2 100644
--- a/test-suite/bugs/closed/shouldsucceed/1834.v
+++ b/test-suite/bugs/closed/shouldsucceed/1834.v
@@ -53,7 +53,7 @@ Definition S1_1 y0 y1 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) :=
    y1 e1.
 
 Definition eq_ok1 y0 y1 y2 (E: eq_1 y0 y1) :=
-  match E with exist e0 e1 => S1_1 y0 y1 e0 e1 = y2 end.
+  match E with exist _ e0 e1 => S1_1 y0 y1 e0 e1 = y2 end.
 
 Definition eq_2 y0 y1 y2 :=
   {E1:eq_1 y0 y1 | eq_ok1 y0 y1 y2 E1}.
@@ -81,7 +81,7 @@ Definition S2_2 y0 y1 y2 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1)
    y2 e2.
 
 Definition eq_ok2 y0 y1 y2 y3 (E: eq_2 y0 y1 y2) : Prop :=
-  match E with exist (exist e0 e1) e2 =>
+  match E with exist _ (exist _ e0 e1) e2 =>
      S2_2 y0 y1 y2 e0 e1 e2 = y3 end.
 
 Definition eq_3 y0 y1 y2 y3 :=
@@ -118,7 +118,7 @@ Definition S3_3 y0 y1 y2 y3 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1)
    y3 e3.
 
 Definition eq_ok3 y0 y1 y2 y3 y4 (E: eq_3 y0 y1 y2 y3) : Prop :=
-  match E with exist (exist (exist e0 e1) e2) e3 =>
+  match E with exist _ (exist _ (exist _ e0 e1) e2) e3 =>
      S3_3 y0 y1 y2 y3 e0 e1 e2 e3 = y4 end.
 
 Definition eq_4 y0 y1 y2 y3 y4 :=
@@ -165,7 +165,7 @@ Definition S4_4 y0 y1 y2 y3 y4 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1)
    y4 e4.
 
 Definition eq_ok4 y0 y1 y2 y3 y4 y5 (E: eq_4 y0 y1 y2 y3 y4) : Prop :=
-  match E with exist (exist (exist (exist e0 e1) e2) e3) e4 =>
+  match E with exist _ (exist _ (exist _ (exist _ e0 e1) e2) e3) e4 =>
      S4_4 y0 y1 y2 y3 y4 e0 e1 e2 e3 e4 = y5 end.
 
 Definition eq_5 y0 y1 y2 y3 y4 y5 :=
diff --git a/test-suite/bugs/closed/shouldsucceed/1891.v b/test-suite/bugs/closed/shouldsucceed/1891.v
index 2d90a2f1dc..685811176a 100644
--- a/test-suite/bugs/closed/shouldsucceed/1891.v
+++ b/test-suite/bugs/closed/shouldsucceed/1891.v
@@ -7,7 +7,7 @@
 
   Lemma L (x: T unit): (unit -> T unit) -> unit.
   Proof.
-    refine (match x return _ with mkT n => fun g => f (g _) end).
+    refine (match x return _ with mkT _ n => fun g => f (g _) end).
     trivial.
   Qed.
 
diff --git a/test-suite/bugs/closed/shouldsucceed/2353.v b/test-suite/bugs/closed/shouldsucceed/2353.v
index b5c45c28c7..baae9a6ece 100644
--- a/test-suite/bugs/closed/shouldsucceed/2353.v
+++ b/test-suite/bugs/closed/shouldsucceed/2353.v
@@ -4,9 +4,9 @@ Inductive term n := app (l : list term n).
 Definition term_list :=
   fix term_size n (t : term n) (acc : nat) {struct t} : nat :=
     match t with
-    | app l =>
+    | app _ l =>
       (fix term_list_size n (l : list term n) (acc : nat) {struct l} : nat :=
       match l with
-      | cons t q => term_list_size (S n) q (term_size n t acc)
+      | cons _ _ t q => term_list_size (S n) q (term_size n t acc)
       end) n l (S acc)
     end.
diff --git a/test-suite/bugs/closed/shouldsucceed/2378.v b/test-suite/bugs/closed/shouldsucceed/2378.v
index 7deec64dd0..ab39633f87 100644
--- a/test-suite/bugs/closed/shouldsucceed/2378.v
+++ b/test-suite/bugs/closed/shouldsucceed/2378.v
@@ -66,9 +66,9 @@ Implicit Arguments lpSat.
 
 Fixpoint LPTransfo Pred1 Pred2 p2lp (f: LP Pred1): LP Pred2 :=
   match f with
-    LPPred p => p2lp p
-  | LPAnd f1 f2 => LPAnd _ (LPTransfo Pred1 Pred2 p2lp f1) (LPTransfo Pred1 Pred2 p2lp f2)
-  | LPNot f1 => LPNot _ (LPTransfo Pred1 Pred2 p2lp f1)
+    LPPred _ p => p2lp p
+  | LPAnd _ f1 f2 => LPAnd _ (LPTransfo Pred1 Pred2 p2lp f1) (LPTransfo Pred1 Pred2 p2lp f2)
+  | LPNot _ f1 => LPNot _ (LPTransfo Pred1 Pred2 p2lp f1)
   end.
 Implicit Arguments LPTransfo.
 
diff --git a/test-suite/bugs/closed/shouldsucceed/2404.v b/test-suite/bugs/closed/shouldsucceed/2404.v
index fe8eba5496..8ac696e912 100644
--- a/test-suite/bugs/closed/shouldsucceed/2404.v
+++ b/test-suite/bugs/closed/shouldsucceed/2404.v
@@ -37,8 +37,8 @@ Definition Rweak : forall a b : bWorld, Type := RstarInv bwweak.
 
 Fixpoint exportRweak {a b} (aRWb : Rweak a b) (y : bName b) : option (bName a) :=
   match aRWb,y with
-  | starReflS a, y' => Some y'
-  | starTransS i j k jWk jRWi, y' =>
+  | starReflS _ a, y' => Some y'
+  | starTransS jWk jRWi, y' =>
     match (bexportw jWk y) with
     | Some x => exportRweak jRWi x
     | None   => None
diff --git a/test-suite/bugs/closed/shouldsucceed/2729.v b/test-suite/bugs/closed/shouldsucceed/2729.v
index 44f8d3c7c9..3efca5d993 100644
--- a/test-suite/bugs/closed/shouldsucceed/2729.v
+++ b/test-suite/bugs/closed/shouldsucceed/2729.v
@@ -53,12 +53,12 @@ Program Fixpoint insertBase {pu : PatchUniverse}
                             (qs : SequenceBase pu mid to)
                           : SequenceBase pu from to
     := match qs with
-       | Nil _ => Cons p Nil
-       | Cons mid' mid2' to' q qs' =>
+       | Nil => Cons p Nil
+       | Cons q qs' =>
            match SignedName_compare (pu_nameOf p) (pu_nameOf q) with
            | Lt => Cons p qs
            | _  => match commutable_dec p (castPatchFrom _ q) with
-                   | inleft (existT _ (existT q' (existT p' _))) => Cons q'
+                   | inleft (existT _ _ (existT _ q' (existT _ p' _))) => Cons q'
 (insertBase p' qs')
                    | inright _ => Cons p qs
                    end
diff --git a/test-suite/bugs/opened/shouldnotfail/1501.v b/test-suite/bugs/opened/shouldnotfail/1501.v
index 1845dd1f60..a0668cd19b 100644
--- a/test-suite/bugs/opened/shouldnotfail/1501.v
+++ b/test-suite/bugs/opened/shouldnotfail/1501.v
@@ -40,11 +40,13 @@ Parameter
 
 Hint Resolve equiv_refl equiv_sym equiv_trans: monad.
 
-Add Relation K equiv
- reflexivity proved by (@equiv_refl)
- symmetry proved by (@equiv_sym)
- transitivity proved by (@equiv_trans)
- as equiv_rel.
+Instance equiv_rel A: Equivalence (@equiv A).
+Proof.
+ constructor.
+ intros xa; apply equiv_refl.
+ intros xa xb; apply equiv_sym.
+ intros xa xb xc; apply equiv_trans.
+Defined.
 
 Definition fequiv (A B: Type)  (f g: A -> K B) := forall (x:A), (equiv (f x) (g
 x)).
@@ -67,17 +69,17 @@ Proof.
   unfold fequiv; intros; eapply equiv_trans; auto with monad.
 Qed.
 
-Add Relation (fun (A B:Type) => A -> K B) fequiv
- reflexivity proved by (@fequiv_refl)
- symmetry proved by (@fequiv_sym)
- transitivity proved by (@fequiv_trans)
- as fequiv_rel.
+Instance fequiv_re A B: Equivalence (@fequiv A B).
+Proof.
+ constructor.
+ intros f; apply fequiv_refl.
+ intros f g; apply fequiv_sym.
+ intros f g h; apply fequiv_trans.
+Defined.
 
-Add Morphism bind
- with signature equiv ==> fequiv ==> equiv
- as bind_mor.
+Instance bind_mor A B: Morphisms.Proper (@equiv _ ==> @fequiv _ _ ==> @equiv _) (@bind A B).
 Proof.
- unfold fequiv; intros; apply bind_compat; auto.
+ unfold fequiv; intros x y xy_equiv f g fg_equiv; apply bind_compat; auto.
 Qed.
 
 Lemma test:
diff --git a/test-suite/bugs/opened/shouldnotfail/1596.v b/test-suite/bugs/opened/shouldnotfail/1596.v
index de77e35d32..22f61ab727 100644
--- a/test-suite/bugs/opened/shouldnotfail/1596.v
+++ b/test-suite/bugs/opened/shouldnotfail/1596.v
@@ -100,6 +100,16 @@ Definition t := (X.t * Y.t)%type.
     left;trivial.
   Defined.
 
+  Definition eq_dec : forall (x y: t), { eq x y } + { ~ eq x y}.
+  Proof.
+    intros [xa xb] [ya yb]; simpl.
+    destruct (X.eq_dec xa ya).
+    destruct (Y.eq_dec xb yb).
+    + left; now split.
+    + right. now intros [eqa eqb].
+    + right. now intros [eqa eqb].
+  Defined.
+
   Hint Immediate eq_sym.
   Hint Resolve eq_refl eq_trans lt_not_eq lt_trans.
 End OrderedPair.
@@ -158,6 +168,14 @@ GT;simpl;trivial;fail).
       apply GT;trivial.
     Defined.
 
+    Definition eq_dec : forall (x y: t), { eq x y } + { ~ eq x y}.
+    Proof.
+    intros [i] [j]. unfold eq.
+    destruct (eq_nat_dec i j).
+    + left. now f_equal.
+    + right. intros meq; now inversion meq.
+    Defined.
+
     Hint Immediate eq_sym.
     Hint Resolve eq_refl eq_trans lt_not_eq lt_trans.
   End Ord.