4 files changed, 15 insertions, 42 deletions
diff --git a/test-suite/bugs/opened/shouldnotfail/1416.v b/test-suite/bugs/opened/shouldnotfail/1416.v
deleted file mode 100644
index c6f4302d..00000000
--- a/test-suite/bugs/opened/shouldnotfail/1416.v
+++ /dev/null
@@ -1,27 +0,0 @@
-Set Implicit Arguments.
-
-Record Place (Env A: Type) : Type := {
-  read: Env -> A ;
-  write: Env -> A -> Env ;
-  write_read: forall (e:Env), (write e (read e))=e
-}. 
-
-Hint Rewrite -> write_read: placeeq.
-
-Record sumPl (Env A B: Type) (vL:(Place Env A)) (vR:(Place Env B)) : Type :=
- { 
-   mkEnv: A -> B -> Env ;
-   mkEnv2writeL: forall (e:Env) (x:A), (mkEnv x (read vR e))=(write vL e x)
- }.
-
-(* when the following line is commented, the bug does not appear *)
-Hint Rewrite -> mkEnv2writeL: placeeq.
-
-Lemma autorewrite_raise_anomaly: forall (Env A:Type) (e: Env) (p:Place Env A),
-  (exists e1:Env, e=(write p e1 (read p e))).
-Proof.
-  intros Env A e p; eapply ex_intro.
-  autorewrite with placeeq. (* Here is the bug *)
-  auto.
-Qed.
-
diff --git a/test-suite/bugs/opened/shouldnotfail/1501.v b/test-suite/bugs/opened/shouldnotfail/1501.v
index 85c09dbd..1845dd1f 100644
--- a/test-suite/bugs/opened/shouldnotfail/1501.v
+++ b/test-suite/bugs/opened/shouldnotfail/1501.v
@@ -8,7 +8,7 @@ Require Export Setoid.
 Section Essais.
 
 (* Parametrized Setoid *)
-Parameter K : Type -> Type. 
+Parameter K : Type -> Type.
 Parameter equiv : forall A : Type, K A -> K A -> Prop.
 Parameter equiv_refl : forall (A : Type) (x : K A), equiv x x.
 Parameter equiv_sym : forall (A : Type) (x y : K A), equiv x y -> equiv y x.
@@ -40,7 +40,7 @@ Parameter
 
 Hint Resolve equiv_refl equiv_sym equiv_trans: monad.
 
-Add Relation K equiv 
+Add Relation K equiv
  reflexivity proved by (@equiv_refl)
  symmetry proved by (@equiv_sym)
  transitivity proved by (@equiv_trans)
@@ -67,7 +67,7 @@ Proof.
   unfold fequiv; intros; eapply equiv_trans; auto with monad.
 Qed.
 
-Add Relation (fun (A B:Type) => A -> K B) fequiv 
+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)
@@ -82,12 +82,12 @@ Qed.
 
 Lemma test:
   forall (A B: Type) (m1 m2 m3: K A) (f: A -> A -> K B),
- (equiv m1 m2) -> (equiv m2 m3) -> 
+ (equiv m1 m2) -> (equiv m2 m3) ->
    equiv (bind m1 (fun a => bind m2 (fun a' => f a a')))
          (bind m2 (fun a => bind m3 (fun a' => f a a'))).
 Proof.
-  intros A B m1 m2 m3 f H1 H2. 
+  intros A B m1 m2 m3 f H1 H2.
   setoid_rewrite H1. (* this works *)
   setoid_rewrite H2.
   trivial by equiv_refl.
-Qed. 
+Qed.
diff --git a/test-suite/bugs/opened/shouldnotfail/1596.v b/test-suite/bugs/opened/shouldnotfail/1596.v
index 766bf524..de77e35d 100644
--- a/test-suite/bugs/opened/shouldnotfail/1596.v
+++ b/test-suite/bugs/opened/shouldnotfail/1596.v
@@ -11,12 +11,12 @@ Module OrderedPair (X:OrderedType) (Y:OrderedType) <: OrderedType with
 Definition t := (X.t * Y.t)%type.
   Definition t := (X.t * Y.t)%type.
 
-  Definition eq (xy1:t) (xy2:t) := 
+  Definition eq (xy1:t) (xy2:t) :=
     let (x1,y1) := xy1 in
       let (x2,y2) := xy2 in
         (X.eq x1 x2) /\ (Y.eq y1 y2).
 
-  Definition lt (xy1:t) (xy2:t) := 
+  Definition lt (xy1:t) (xy2:t) :=
     let (x1,y1) := xy1 in
       let (x2,y2) := xy2 in
         (X.lt x1 x2) \/ ((X.eq x1 x2) /\ (Y.lt y1 y2)).
@@ -101,7 +101,7 @@ Definition t := (X.t * Y.t)%type.
   Defined.
 
   Hint Immediate eq_sym.
-  Hint Resolve eq_refl eq_trans lt_not_eq lt_trans. 
+  Hint Resolve eq_refl eq_trans lt_not_eq lt_trans.
 End OrderedPair.
 
 Module MessageSpi.
@@ -189,8 +189,8 @@ n)->(hedge_synthesis_relation h m n).
 
   Fixpoint hedge_in_synthesis (h:hedge) (m:MessageSpi.message)
 (n:MessageSpi.message) {struct m} : bool :=
-    if H.mem (m,n) h 
-      then true 
+    if H.mem (m,n) h
+      then true
       else false.
 
   Definition hedge_synthesis_spec (h:hedge) := hedge_synthesis_relation
@@ -221,8 +221,8 @@ n).
 
   Fixpoint hedge_in_synthesis (h:hedge) (m:MessageSpi.t) (n:MessageSpi.t)
 {struct m} : bool :=
-    if H.mem (m,n) h 
-      then true 
+    if H.mem (m,n) h
+      then true
       else false.
 
   Definition hedge_synthesis_spec (h:hedge) := hedge_synthesis_relation
@@ -235,7 +235,7 @@ n).
     induction m;simpl;intro.
     elim (Bool_elim_bool (H.mem (MessageSpi.MNam n,n0) h));intros.
     apply SynInc;apply H.mem_2;trivial.
-    
+
     rewrite H in H0. (* !! impossible here !! *)
     discriminate H0.
   Qed.
diff --git a/test-suite/bugs/opened/shouldnotfail/1671.v b/test-suite/bugs/opened/shouldnotfail/1671.v
index 800c431e..d95c2108 100644
--- a/test-suite/bugs/opened/shouldnotfail/1671.v
+++ b/test-suite/bugs/opened/shouldnotfail/1671.v
@@ -6,7 +6,7 @@ CoInductive hdlist : unit -> Type :=
 Variable P : forall bo, hdlist bo -> Prop.
 Variable all : forall bo l, P bo l.
 
-Definition F (l:hdlist tt) : P tt l := 
+Definition F (l:hdlist tt) : P tt l :=
 match l in hdlist u return P u l with
 | cons (cons l') => all tt _
 end.