diff --git a/CHANGES.md b/CHANGES.md
index 05f0795da..37d0ceab8 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -21,6 +21,8 @@
 
 ## Improved
 
+-  Pattern-matching redundancy is now a warning instead of an error.
+  [\#222](https://github.com/ocaml-gospel/gospel/pull/222)
 - Allow unit result in function header
   [\#215](https://github.com/ocaml-gospel/gospel/pull/215)
 - Highlight source locations when reporting errors.
diff --git a/src/patmat.ml b/src/patmat.ml
index 61d214464..e0e511a4a 100644
--- a/src/patmat.ml
+++ b/src/patmat.ml
@@ -568,4 +568,4 @@ let checks ~loc ty cases =
     let tyl = ty :: bools in
     check_exhaustive ~loc tyl pmat q bools;
     check_redundancy ~loc tyl pmat
-  with W.Warning e -> Fmt.epr "%a@." W.pp_warn e
+  with W.Warning e -> Fmt.pr "%a@." W.pp_warn e
diff --git a/test/patterns/negative/redundant1.mli b/test/patterns/negative/redundant1.mli
index 501b26bcd..e7cea53df 100644
--- a/test/patterns/negative/redundant1.mli
+++ b/test/patterns/negative/redundant1.mli
@@ -4,11 +4,12 @@ val f : int -> int
     | _ -> true
     | 1i -> false *)
 (* {gospel_expected|
-   [125] File "redundant1.mli", line 3, characters 12-58:
-         3 | ............match x with
-         4 |     | _ -> true
-         5 |     | 1i -> false...
-         Error: The pattern-matching is redundant.
+   [0] File "redundant1.mli", line 3, characters 12-58:
+       3 | ............match x with
+       4 |     | _ -> true
+       5 |     | 1i -> false...
+       Warning: The pattern-matching is redundant.
                 Here is a case that is unused:
                   1i.
+       OK
    |gospel_expected} *)
diff --git a/test/patterns/negative/redundant2.mli b/test/patterns/negative/redundant2.mli
index 47058d3df..745792781 100644
--- a/test/patterns/negative/redundant2.mli
+++ b/test/patterns/negative/redundant2.mli
@@ -8,13 +8,14 @@ val f : t -> int
     | B (B A) -> false
     | _ -> true *)
 (* {gospel_expected|
-   [125] File "redundant2.mli", line 5, characters 12-103:
-         5 | ............match x with
-         6 |     | A -> false
-         7 |     | B (B _) -> false
-         8 |     | B (B A) -> false
-         9 |     | _ -> true...
-         Error: The pattern-matching is redundant.
+   [0] File "redundant2.mli", line 5, characters 12-103:
+       5 | ............match x with
+       6 |     | A -> false
+       7 |     | B (B _) -> false
+       8 |     | B (B A) -> false
+       9 |     | _ -> true...
+       Warning: The pattern-matching is redundant.
                 Here is a case that is unused:
                   B B A.
+       OK
    |gospel_expected} *)
diff --git a/test/patterns/negative/redundant3.mli b/test/patterns/negative/redundant3.mli
index 08bb1a575..9f39921ff 100644
--- a/test/patterns/negative/redundant3.mli
+++ b/test/patterns/negative/redundant3.mli
@@ -7,12 +7,13 @@ val f : t -> int
     | B (B A) -> false
     | _ -> true *)
 (* {gospel_expected|
-   [125] File "redundant3.mli", line 5, characters 12-86:
-         5 | ............match x with
-         6 |     | A | B _ -> false
-         7 |     | B (B A) -> false
-         8 |     | _ -> true...
-         Error: The pattern-matching is redundant.
+   [0] File "redundant3.mli", line 5, characters 12-86:
+       5 | ............match x with
+       6 |     | A | B _ -> false
+       7 |     | B (B A) -> false
+       8 |     | _ -> true...
+       Warning: The pattern-matching is redundant.
                 Here is a case that is unused:
                   B B A.
+       OK
    |gospel_expected} *)