blob: cd1a692f5490b10e13c6bdaa8f5988c20e2ccfe1 (
plain)
1
2
3
4
|
- Added ``#[refine]`` attribute for :cmd:`Instance`, a more
predictable version of the old ``Refine Instance Mode`` which
unconditionally opens a proof (`#10996
<https://github.com/coq/coq/pull/10996>`_, by Gaëtan Gilbert).
|
