diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2014-04-29 23:20:42 -0400 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2014-04-29 23:57:48 -0400 |
| commit | 1c7756adb95a70f8d382be062cc2d68bcf37e5a9 (patch) | |
| tree | 6e1f4dfb264a73d75bb23a289f456405432ff15c /coq.itarget | |
| parent | 6acf543800fe176ca7d47ef7165ebc14588efb6f (diff) | |
Injection: do not fail when arguments have sort Prop.
This historic limitation of the injection tactic does not seem to have any
precise justification. In fact, the only equalities that are not projectable is
when the arguments of the constructor have sort Set or Type and the inductive
type is in Prop (due to the restriction on pattern matching).
The command "Unset Injection On Proofs" restores the old behavior.
Diffstat (limited to 'coq.itarget')
0 files changed, 0 insertions, 0 deletions