aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-10-19 15:43:39 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-10-19 17:05:39 +0200
commit21e1d501e17c9989d9cd689988a510e1864f817a (patch)
tree2bb19e8fe38ad80c2cb3266eaba47aa85d9906c7 /test-suite/output
parent6fbe3c850bac9cbdfa64dbdcca7bd60dc7862190 (diff)
Attempt to improve error rendering in pattern-matching compilation (#5142).
When trying different possible return predicates, returns the error given by the first try, assuming this is the most interesting one.
Diffstat (limited to 'test-suite/output')
-rw-r--r--test-suite/output/Cases.out3
-rw-r--r--test-suite/output/Cases.v12
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.