diff options
| author | Hugo Herbelin | 2014-10-30 13:23:10 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-31 18:49:05 +0100 |
| commit | b2e1d4ea930c07ca27168fb43908a32d1101fce0 (patch) | |
| tree | ab08a3b0492ef8c3a6050c638540efdd12b86c82 /dev | |
| parent | cfb5201e2ebc2516e3de7c578355db8bd4f08d35 (diff) | |
Avoid "destruct H" to apply on H itself when H is a section variable.
Need some contorsion for not using the general scheme of naming based
which uses the hypothesis name as base ident, and for instead keeping
a name generated on the type of the section variable, as it was before
for section variables (example of incompatibility in FMapPositive).
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions
