diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2014-05-18 13:05:42 -0400 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2014-05-18 13:05:42 -0400 |
| commit | 12b121057d03558b9f1eec76f1cc72bc12c9b699 (patch) | |
| tree | c60d4d2ab59c1073be9bce502f62a61d8382e56f /theories/QArith | |
| parent | 076274d366f7dd4f09d99fa8f3962b6f78bf9252 (diff) | |
When discrimination is not possible, try to project.
Example:
Inductive Pnat : Prop := O | S : Pnat -> Pnat.
Variable m n : Pnat.
Goal S (S O) = S O -> False.
intros H; injection H.
now deduces S O = O instead of failing with an error message.
Diffstat (limited to 'theories/QArith')
0 files changed, 0 insertions, 0 deletions