diff options
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 36 |
1 files changed, 19 insertions, 17 deletions
@@ -7,6 +7,22 @@ Tactics Use with Set Default Goal Selector to force focusing before tactics are called. +- The undocumented "nameless" forms `fix N`, `cofix` that were + deprecated in 8.8 have been removed from LTAC's syntax; please use + `fix ident N/cofix ident` to explicitely name the (co)fixpoint + hypothesis to be introduced. + +- Introduction tactics "intro"/"intros" on a goal which is an + existential variable now force a refinement of the goal into a + dependent product rather than failing. + +- Support for fix/cofix added in Ltac "match" and "lazymatch". + +- Ltac backtraces now include trace information about tactics + called by OCaml-defined tactics. + +- Option "Ltac Debug" now applies also to terms built using Ltac functions. + Tools - Coq_makefile lets one override or extend the following variables from @@ -22,20 +38,6 @@ Vernacular Commands By default, they are disabled and produce an error. The deprecation warning which used to occur when using nested proofs has been removed. -Tactics - -- Introduction tactics "intro"/"intros" on a goal which is an - existential variable now force a refinement of the goal into a - dependent product rather than failing. - -Tactic language - -- Support for fix/cofix added in Ltac "match" and "lazymatch". - -- Ltac backtraces now include trace information about tactics - called by OCaml-defined tactics. -- Option "Ltac Debug" now applies also to terms built using Ltac functions. - Coq binaries and process model - Before 8.9, Coq distributed a single `coqtop` binary and a set of @@ -67,9 +69,9 @@ Tools Tactic language -- The undocumented "nameless" forms `fix N`, `cofix N` have been - deprecated; please use `fix/cofix ident N` to explicitely name - hypothesis to be introduced. +- The undocumented "nameless" forms `fix N`, `cofix` have been + deprecated; please use `fix ident N /cofix ident` to explicitely + name the (co)fixpoint hypothesis to be introduced. Documentation |