From 44d2955e49110a401d88c0449583b8c833887d9d Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 22 Mar 2020 12:27:29 +0100 Subject: Removing deprecated destruct syntax _eqn. --- doc/sphinx/language/gallina-specification-language.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 12a9a30f3d..3b64465120 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -117,7 +117,7 @@ Other tokens ! #[ % & ' ( () (bfs) (dfs) ) * ** + , - -> . .( .. ... / : ::= := :> :>> ; < <+ <- <: - <<: <= = => > >-> >= ? @ @{ [ [= ] _ _eqn + <<: <= = => > >-> >= ? @ @{ [ [= ] _ `( `{ { {| | |- || } When multiple tokens match the beginning of a sequence of characters, -- cgit v1.2.3 From 274ed99f9964b802e0a340c39ad69de4cabf37ff Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 22 Mar 2020 15:24:43 +0100 Subject: Change log Co-Authored-By: Théo Zimmermann --- doc/changelog/04-tactics/11877-master+deprecated-_eqn.rst | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 doc/changelog/04-tactics/11877-master+deprecated-_eqn.rst (limited to 'doc') diff --git a/doc/changelog/04-tactics/11877-master+deprecated-_eqn.rst b/doc/changelog/04-tactics/11877-master+deprecated-_eqn.rst new file mode 100644 index 0000000000..827d484b28 --- /dev/null +++ b/doc/changelog/04-tactics/11877-master+deprecated-_eqn.rst @@ -0,0 +1,5 @@ +- **Removed:** + Deprecated syntax `_eqn` for :tacn:`destruct` and :tacn:`remember`. + Use `eqn:` syntax instead + (`#11877 `_, + by Hugo Herbelin). -- cgit v1.2.3