aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog/02-specification-language/10996-refine-instance-returns.rst
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).