diff options
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 22 |
1 files changed, 22 insertions, 0 deletions
@@ -11,6 +11,15 @@ Notations priority is given to latest notations defined in the scopes being opened rather than to the latest notations defined independently of whether they are in an opened scope or not. +- Notations can now refer to the syntactic category of patterns (as in + "fun 'pat =>" or "match p with pat => ... end"). Two variants are + available, depending on whether a single variable is considered as a + pattern or not. +- Recursive notations now support ".." patterns with several + occurrences of the recursive term or binder, possibly mixing terms + and binders, possibly in reverse left-to-right order. +- "Locate" now working also on notations of the form "x + y" (rather + than "_ + _"). Specification language @@ -32,6 +41,7 @@ Tactics such as "x := 5 : Z" (see BZ#148). This could be disabled via Unset Omega UseLocalDefs. - The tactic "romega" is also aware now of the bodies of context variables. +- The tactic "zify" resp. "omega with N" is now aware of N.pred. - Tactic "decide equality" now able to manage constructors which contain proofs. - Added tactics reset ltac profile, show ltac profile (and variants) @@ -44,6 +54,9 @@ Tactics with let bindings in the parameters. - The tactic "dtauto" now handles some inductives such as "@sigT A (fun _ => B)" as non-dependent conjunctions. +- A bug fixed in "rewrite H in *" and "rewrite H in * |-" may cause a + few rare incompatibilities (it was unintendedly recursively + rewriting in the side conditions generated by H). Focusing @@ -89,6 +102,15 @@ Documentation moved to the GitHub wiki section of this repository; the main entry page is https://github.com/coq/coq/wiki/The-Coq-FAQ. +Standard Library + +- New libraries Coq.Init.Decimal, Coq.Numbers.DecimalFacts, + Coq.Numbers.DecimalNat, Coq.Numbers.DecimalPos, + Coq.Numbers.DecimalN, Coq.Numbers.DecimalZ, + Coq.Numbers.DecimalString providing a type of decimal numbers, some + facts about them, and conversions between decimal numbers and nat, + positive, N, Z, and string. + Changes from 8.7.1 to 8.7.2 =========================== |