blob: 54417077f5362c42bd2ec47b20f95dbf70225d3a (
plain)
1
2
3
4
5
6
|
- Add command line options `-require-import`, `-require-export`,
`-require-import-from` and `-require-export-from`, as well as their
shorthand, `-ri`, `-re`, `-refrom` and -`rifrom`. Deprecate
confusing command line option `-require`
(`#10245 <https://github.com/coq/coq/pull/10245>`_
by Hugo Herbelin, review by Emilio Gallego).
|
