diff options
author | 2016-12-22 21:32:35 +0100 | |
---|---|---|
committer | 2016-12-22 21:54:26 +0100 | |
commit | f5575393258492837d3764d07f8290b576f61160 (patch) | |
tree | 18d33a63880226185f6fb3cd8b6f31cb3e965a28 /test-suite/success/Discriminate.v | |
parent | 59e361cd4118fdb974081fc0b2aec02136fde444 (diff) |
Fixing injection in the presence of let-in in constructors.
This also fixes decide equality, discriminate, ... (see e.g. #5279).
Diffstat (limited to 'test-suite/success/Discriminate.v')
-rw-r--r-- | test-suite/success/Discriminate.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/success/Discriminate.v b/test-suite/success/Discriminate.v index a75967411..6abfca4c3 100644 --- a/test-suite/success/Discriminate.v +++ b/test-suite/success/Discriminate.v @@ -38,3 +38,10 @@ Abort. Goal ~ identity 0 1. discriminate. Qed. + +(* Check discriminate on types with local definitions *) + +Inductive A := B (T := unit) (x y : bool) (z := x). +Goal forall x y, B x true = B y false -> False. +discriminate. +Qed. |