diff options
| author | Théo Zimmermann | 2019-05-19 16:26:24 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-05-19 16:26:24 +0200 |
| commit | 8bd60579d4768793c849b9b4cd46f14d33d0f71d (patch) | |
| tree | 9fb0510584dae4f5416f8776b26cd7964ceb810f /doc/sphinx/changes.rst | |
| parent | e3e8dfb4c2f30ed1c6715999e1f74914e7bc187b (diff) | |
| parent | feb9c50b5812a01e9dc60e2408f4f9f38986ce8c (diff) | |
Merge PR #10143: Add dedicated syntax for alternatives (abc | def) in manual notations
Reviewed-by: Zimmi48
Ack-by: jfehrle
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 cca3b2e06b..5e337bcef0 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -498,7 +498,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). @@ -3940,7 +3940,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 |