diff options
| author | Clément Pit-Claudel | 2019-05-10 22:29:57 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2019-05-16 11:59:12 -0400 |
| commit | feb9c50b5812a01e9dc60e2408f4f9f38986ce8c (patch) | |
| tree | f35a5b763eb5fb2c6041928089508aebf154b351 /doc/sphinx/changes.rst | |
| parent | f3f758896b82d34acd0e42a65f08a5cb80aa0da9 (diff) | |
[refman] Introduce syntax for alternatives in notations
Closes GH-8482.
Diffstat (limited to 'doc/sphinx/changes.rst')
| -rw-r--r-- | doc/sphinx/changes.rst | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 5704587ae0..e54c1a4eec 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -457,7 +457,7 @@ Other changes in 8.10+beta1 - Command :cmd:`Instance`, when no body is provided, now always opens a proof. This is a breaking change, as instance of :n:`Instance @ident__1 : @ident__2.` where :n:`@ident__2` is a trivial class will - have to be changed into :n:`Instance @ident__1 : @ident__2 := {}.` + have to be changed into :n:`Instance @ident__1 : @ident__2 := %{%}.` or :n:`Instance @ident__1 : @ident__2. Proof. Qed.` (`#9274 <https://github.com/coq/coq/pull/9274>`_, by Maxime Dénès). @@ -3881,7 +3881,7 @@ Vernacular commands Equality Schemes", this replaces deprecated option "Equality Scheme"). - Made support for automatic generation of case analysis schemes available to user (governed by option "Set Case Analysis Schemes"). -- New command :n:`{? Global } Generalizable [All|No] [Variable|Variables] {* @ident}` to +- New command :n:`{? Global } Generalizable {| All | No } {| Variable | Variables } {* @ident}` to declare which identifiers are generalizable in `` `{} `` and `` `() `` binders. - New command "Print Opaque Dependencies" to display opaque constants in addition to all variables, parameters or axioms a theorem or |