diff options
author | 2017-11-28 19:49:02 +0100 | |
---|---|---|
committer | 2017-11-28 22:04:41 +0100 | |
commit | 08da05299d32886bb516124fa497347b40249006 (patch) | |
tree | 14d186a8ae04c09ab6f1e13eb0e204a7b5867519 /proofs/proof_global.mli | |
parent | 4b4e8b2b022c73bf0e73c28e60e2dc05fd0dbf8e (diff) |
In injection/inversion, consider all template-polymorphic types as injectable.
In particular singleton inductive types are considered injectable,
even in the absence of the option "Set Keep Proof Equalities".
This fixes #3125 (and #4560, #6273).
Diffstat (limited to 'proofs/proof_global.mli')
0 files changed, 0 insertions, 0 deletions