diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-10-06 12:39:18 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-10-06 12:39:18 +0200 |
commit | ef11a1240c14560e199527ae6d8a6eb893da1438 (patch) | |
tree | fb2b2df5d56d97fafbf65a116c416dabca07808b /lib/flags.mli | |
parent | 3134ddd5dae8c9ab78a8aad181b2142f63907ecb (diff) | |
parent | d24bab45123f4e4eb3918be55fb1a7dc54be2b3b (diff) |
Merge PR #1121: Fixing BZ#5765 (an anomaly with 'pat in the parameters of an inductive definition)
Diffstat (limited to 'lib/flags.mli')
0 files changed, 0 insertions, 0 deletions