Unset Asymmetric Patterns

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

2 files changed, 34 insertions, 14 deletions

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.