diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-19 15:43:39 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-19 17:05:39 +0200 |
commit | 21e1d501e17c9989d9cd689988a510e1864f817a (patch) | |
tree | 2bb19e8fe38ad80c2cb3266eaba47aa85d9906c7 /test-suite/output | |
parent | 6fbe3c850bac9cbdfa64dbdcca7bd60dc7862190 (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.out | 3 | ||||
-rw-r--r-- | test-suite/output/Cases.v | 12 |
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. |