blob: 51a62a0c8d21d3fcf728df467ef530b11c3a36f1 (
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).
|