diff options
| author | Théo Zimmermann | 2018-10-02 16:22:27 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-10-02 16:22:27 +0200 |
| commit | 7803262696980e6f2cb1fd4397b91f1098712647 (patch) | |
| tree | 1b85870819e2b75019dda5c5460a885b7d921b14 | |
| parent | e65d160d5fa4e0b8b5754b0925b0b5a880523bc5 (diff) | |
| parent | 2d31d956fb708add948d0126b7c616375abf6358 (diff) | |
Merge PR #8620: Docs: Missing backquote
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 636144e0c8..9dae7fd102 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -606,7 +606,7 @@ for several ways of defining a function *and other useful related objects*, namely: an induction principle that reflects the recursive structure of the function (see :tacn:`function induction`) and its fixpoint equality. The meaning of this declaration is to define a function ident, -similarly to ``Fixpoint`. Like in ``Fixpoint``, the decreasing argument must +similarly to ``Fixpoint``. Like in ``Fixpoint``, the decreasing argument must be given (unless the function is not recursive), but it might not necessarily be *structurally* decreasing. The point of the {} annotation is to name the decreasing argument *and* to describe which kind of |