Skip to content

2.4.0
Compare
Choose a tag to compare
@fblanqui fblanqui released this 31 Jul 12:11
· 91 commits to master since this release
2.4.0
193d86c

CHANGES:

Added

  • Several options for export -o stt_coq.
  • Tactic remove.
  • Option --no-sr-check to disable subject reduction checking.
  • CLI command index to build ~/.LPSearch.db.
  • Indexed terms can be normalized wrt rules with the option --rules
    (note that this new option --rules could be used to implement the equivalent
    of dkmeta later).
  • CLI command search and LP command search to send queries to the index.
  • Query language.
  • CLI command websearch to run a webserver that can answer search queries.
  • Option --port to specify the port to use.

Improved

  • Output for export -o stt_coq.

Changed

  • Private definitions are not kept in memory and in lpo files anymore.
  • The record type Eval.config is extended with a new field allowing to specify
    which dtree to use for each symbol.
Assets 3
Loading