Bug fixed by Hugo.

1 files changed, 3 insertions, 3 deletions

diff --git a/test-suite/bugs/opened/3388.v b/test-suite/bugs/closed/3388.v
index d0ea72e1fd..7826280498 100644
--- a/test-suite/bugs/opened/3388.v
+++ b/test-suite/bugs/closed/3388.v
@@ -5,7 +5,7 @@ Inductive test : bool -> bool -> Type :=
 .
 
 (* This does not work *)
-Fail Definition test_a (t : test true false) : test true false :=
+Definition test_a (t : test true false) : test true false :=
   match t with
     | test10 => test10
   end.
@@ -44,14 +44,14 @@ Definition test2_a (t : test2 true false) : test2 true false :=
   end.
 
 (* Accordingly, this now fails *)
-Fail Definition test2_b (t : test2 false true) : test2 false true :=
+Definition test2_b (t : test2 false true) : test2 false true :=
   match t with
     | test201 => test201
   end.
 
 
 (* This, too, fails *)
-Fail Definition test2_c x (t : test2 false x) : test2 false x :=
+Definition test2_c x (t : test2 false x) : test2 false x :=
   match t with
     | test201 => test201
   end.