diff options
| author | Joachim Breitner | 2018-10-01 22:09:33 -0700 |
|---|---|---|
| committer | Joachim Breitner | 2018-10-01 22:09:33 -0700 |
| commit | 2d31d956fb708add948d0126b7c616375abf6358 (patch) | |
| tree | e9dbebc3c0d4d8e203eebdb14f394e68fd39de62 | |
| parent | 05786b23cf0d031c93998c59f6f2f94d6049b027 (diff) | |
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 |