diff options
Diffstat (limited to 'doc/sphinx/changes.rst')
| -rw-r--r-- | doc/sphinx/changes.rst | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index cc2c43e7dd..701c62cdce 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -186,7 +186,7 @@ Coq is now continuously tested against OCaml trunk, in addition to the oldest supported and latest OCaml releases. Coq's documentation for the development branch is now deployed -continously at https://coq.github.io/doc/master/api (documentation of +continuously at https://coq.github.io/doc/master/api (documentation of the ML API), https://coq.github.io/doc/master/refman (reference manual), and https://coq.github.io/doc/master/stdlib (documentation of the standard library). Similar links exist for the `v8.10` branch. @@ -665,7 +665,7 @@ changes: - New commands :cmd:`Hint Variables` and :cmd:`Hint Constants`, by Matthieu Sozeau, for controlling the opacity status of variables and constants in hint databases. It is recommended to always use these - commands after creating a hint databse with :cmd:`Create HintDb`. + commands after creating a hint database with :cmd:`Create HintDb`. - Multiple sections with the same name are now allowed, by Jasper Hugunin. @@ -892,7 +892,7 @@ Vernacular Commands `Inductive list (A : Type) := nil : list | cons : A -> list -> list.` - New `Set Hint Variables/Constants Opaque/Transparent` commands for setting globally the opacity flag of variables and constants in hint databases, - overwritting the opacity set of the hint database. + overwriting the opacity set of the hint database. - Added generic syntax for "attributes", as in: `#[local] Lemma foo : bar.` - Added the `Numeral Notation` command for registering decimal numeral @@ -1129,7 +1129,7 @@ Tactics few rare incompatibilities (it was unintendedly recursively rewriting in the side conditions generated by H). - Added tactics "assert_succeeds tac" and "assert_fails tac" to ensure - properties of the executation of a tactic without keeping the effect + properties of the execution of a tactic without keeping the effect of the execution. - `vm_compute` now supports existential variables. - Calls to `shelve` and `give_up` within calls to tactic `refine` now working. @@ -1262,7 +1262,7 @@ Tools Tactic language - The undocumented "nameless" forms `fix N`, `cofix` have been - deprecated; please use `fix ident N /cofix ident` to explicitely + deprecated; please use `fix ident N /cofix ident` to explicitly name the (co)fixpoint hypothesis to be introduced. Documentation @@ -2953,7 +2953,7 @@ Other bugfixes - Fix incorrect behavior of CS resolution - #4591: Uncaught exception in directory browsing. - CoqIDE is more resilient to initialization errors. -- #4614: "Fully check the document" is uninterruptable. +- #4614: "Fully check the document" is uninterruptible. - Try eta-expansion of records only on non-recursive ones - Fix bug when a sort is ascribed to a Record - Primitive projections: protect kernel from erroneous definitions. @@ -3442,7 +3442,7 @@ Libraries * all functions over type Z : Z.add, Z.mul, ... * the minimal proofs of specifications for these functions : Z.add_0_l, ... - * an instantation of all derived properties proved generically in Numbers : + * an instantiation of all derived properties proved generically in Numbers : Z.add_comm, Z.add_assoc, ... A large part of ZArith is now simply compatibility notations, for instance @@ -4623,7 +4623,7 @@ Setoid rewriting + Setoid_Theory is now an alias to Equivalence, scripts building objects of type Setoid_Theory need to unfold (or "red") the definitions of Reflexive, Symmetric and Transitive in order to get the same goals - as before. Scripts which introduced variables explicitely will not break. + as before. Scripts which introduced variables explicitly will not break. + The order of subgoals when doing [setoid_rewrite] with side-conditions is always the same: first the new goal, then the conditions. @@ -5022,7 +5022,7 @@ Syntax Language and commands -- Added sort-polymorphism for definitions in Type (but finally abandonned). +- Added sort-polymorphism for definitions in Type (but finally abandoned). - Support for implicit arguments in the types of parameters in (co-)fixpoints and (co-)inductive declarations. - Improved type inference: use as much of possible general information. @@ -5251,7 +5251,7 @@ Library - New file about the factorial function in Arith -- An additional elimination Acc_iter for Acc, simplier than Acc_rect. +- An additional elimination Acc_iter for Acc, simpler than Acc_rect. This new elimination principle is used for definition well_founded_induction. - New library NArith on binary natural numbers @@ -5336,7 +5336,7 @@ Bugs Miscellaneous - Implicit parameters of inductive types definition now taken into - account for infering other implicit arguments + account for inferring other implicit arguments Incompatibilities @@ -5417,7 +5417,7 @@ Gallina Known problems of the automatic translation - iso-latin-1 characters are no longer supported: move your files to - 7-bits ASCII or unicode before translation (swith to unicode is + 7-bits ASCII or unicode before translation (switch to unicode is automatically done if a file is loaded and saved again by coqide) - Renaming in ZArith: incompatibilities in Coq user contribs due to merging names INZ, from Reals, and inject_nat. @@ -5442,7 +5442,7 @@ Vernacular commands - "Functional Scheme" and "Functional Induction" extended to polymorphic types and dependent types - Notation now allows recursive patterns, hence recovering parts of the - fonctionalities of pre-V8 Grammar/Syntax commands + functionalities of pre-V8 Grammar/Syntax commands - Command "Print." discontinued. - Redundant syntax "Implicit Arguments On/Off" discontinued |