diff options
| -rw-r--r-- | CHANGES | 7 |
1 files changed, 7 insertions, 0 deletions
@@ -133,6 +133,13 @@ Plugins - The mathematical proof language (also known as declarative mode) was removed. - A new command Extraction TestCompile has been introduced, not meant for the general user but instead for Coq's test-suite. +- The extraction plugin is no longer loaded by default. It must be + explicitly loaded with [Require Extraction], which is backwards + compatible. +- The functional induction plugin (which provides the [Function] + vernacular) is no longer loaded by default. It must be explicitly + loaded with [Require FunInd], which is backwards compatible. + Dependencies |