diff options
| author | Hugo Herbelin | 2020-03-22 12:27:29 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-26 18:00:08 +0100 |
| commit | 44d2955e49110a401d88c0449583b8c833887d9d (patch) | |
| tree | 8e5357f9316628595f1216bc8fd753287921e01b /doc | |
| parent | 63f2da5b3703a16c7722b91ce2f2c78617dec9a7 (diff) | |
Removing deprecated destruct syntax _eqn.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 2 |
1 files changed, 1 insertions, 1 deletions
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, |