aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.doc
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-10-30 13:23:10 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-10-31 18:49:05 +0100
commitb2e1d4ea930c07ca27168fb43908a32d1101fce0 (patch)
treeab08a3b0492ef8c3a6050c638540efdd12b86c82 /Makefile.doc
parentcfb5201e2ebc2516e3de7c578355db8bd4f08d35 (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 'Makefile.doc')
0 files changed, 0 insertions, 0 deletions