Skip to content

Commit 2a27c28

Browse files
add CHANGES.md entry
1 parent 8d99e54 commit 2a27c28

1 file changed

Lines changed: 1 addition & 0 deletions

File tree

CHANGES.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
2222
- Tactic `#print` to print a symbol or the current goal.
2323
- Export to Lean.
2424
- Tactic `all_hyps t` calls parameterized tactic term t on all hypotheses ignoring failing calls.
25+
- LSP server: completion (in-scope symbols; tactic keywords and goal hypotheses inside proofs), hierarchical document symbols, go-to-definition on `require`/`open` module paths, `didChange` debouncing, and an integration test suite (`make test_lsp`).
2526

2627
### Changed
2728

0 commit comments

Comments
 (0)