From df8df4637dfb4106854554cc2ac94b4fdd565e80 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 19 Apr 2020 13:00:09 +0200
Subject: Fixing #11903: Fixpoints not truly recursive in standard library.

There was also a non truly recursive in the doc.
---
 doc/sphinx/proof-engine/ssreflect-proof-language.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 28c5359a04..4be18ccda9 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -286,7 +286,7 @@ example, the null and all list function(al)s can be defined as follows:
    .. coqtop:: all
 
       Variable d: Set.
-      Fixpoint null (s : list d) :=
+      Definition null (s : list d) :=
         if s is nil then true else false.
       Variable a : d -> bool.
       Fixpoint all (s : list d) : bool :=
-- 
cgit v1.2.3