2 files changed, 15 insertions, 0 deletions
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 2b828d382..95fcd362e 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -56,3 +56,6 @@ match H with
      else fun _ : P false => Logic.I) x
 end
      : B -> True
+The command has indeed failed with message:
+Non exhaustive pattern-matching: no clause found for pattern 
+gadtTy _ _
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 3c2eaf42c..1903753cc 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -77,3 +77,15 @@ destruct b as [|] ; exact Logic.I.
 Defined.
 
 Print f.
+
+(* Was enhancement request #5142 (error message reported on the most
+   general return clause heuristic) *)
+
+Inductive gadt : Type -> Type :=
+| gadtNat : nat -> gadt nat
+| gadtTy : forall T, T -> gadt T.
+
+Fail Definition gadt_id T (x: gadt T) : gadt T :=
+  match x with
+  | gadtNat n => gadtNat n
+  end.