Fixing #11903: Fixpoints not truly recursive in standard library.

There was also a non truly recursive in the doc.

7 files changed, 11 insertions, 11 deletions

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 :=
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index f78c0ecc1e..ad0124db6d 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -123,7 +123,7 @@ Definition create l x e r :=
 
 Definition assert_false := create.
 
-Fixpoint bal l x d r :=
+Definition bal l x d r :=
   let hl := height l in
   let hr := height r in
   if gt_le_dec hl (hr+2) then
@@ -191,7 +191,7 @@ Fixpoint remove_min l x d r : t*(key*elt) :=
   [|height t1 - height t2| <= 2].
 *)
 
-Fixpoint merge s1 s2 :=  match s1,s2 with
+Definition merge s1 s2 :=  match s1,s2 with
   | Leaf, _ => s2
   | _, Leaf => s1
   | _, Node l2 x2 d2 r2 h2 =>
diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v
index 855db8bc3f..2a84456500 100644
--- a/theories/Init/Decimal.v
+++ b/theories/Init/Decimal.v
@@ -179,7 +179,7 @@ Definition del_head_int n d :=
 (** [del_tail n d] removes [n] digits at end of [d]
     or returns [zero] if [d] has less than [n] digits. *)
 
-Fixpoint del_tail n d := rev (del_head n (rev d)).
+Definition del_tail n d := rev (del_head n (rev d)).
 
 Definition del_tail_int n d :=
   match d with
diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v
index ea53618acb..04685cc3eb 100644
--- a/theories/NArith/BinNatDef.v
+++ b/theories/NArith/BinNatDef.v
@@ -126,7 +126,7 @@ Infix "?=" := compare (at level 70, no associativity) : N_scope.
 
 (** Boolean equality and comparison *)
 
-Fixpoint eqb n m :=
+Definition eqb n m :=
   match n, m with
     | 0, 0 => true
     | pos p, pos q => Pos.eqb p q
@@ -313,7 +313,7 @@ Definition land n m :=
 
 (** Logical [diff] *)
 
-Fixpoint ldiff n m :=
+Definition ldiff n m :=
  match n, m with
   | 0, _ => 0
   | _, 0 => n
diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v
index 55b9ec4a44..c05ed9ebf4 100644
--- a/theories/ZArith/BinIntDef.v
+++ b/theories/ZArith/BinIntDef.v
@@ -208,7 +208,7 @@ Definition gtb x y :=
     | _ => false
   end.
 
-Fixpoint eqb x y :=
+Definition eqb x y :=
   match x, y with
     | 0, 0 => true
     | pos p, pos q => Pos.eqb p q
diff --git a/theories/extraction/ExtrOcamlBigIntConv.v b/theories/extraction/ExtrOcamlBigIntConv.v
index 7740bb41d9..29bd732c78 100644
--- a/theories/extraction/ExtrOcamlBigIntConv.v
+++ b/theories/extraction/ExtrOcamlBigIntConv.v
@@ -45,14 +45,14 @@ Fixpoint bigint_of_pos p :=
   | xI p => bigint_succ (bigint_twice (bigint_of_pos p))
  end.
 
-Fixpoint bigint_of_z z :=
+Definition bigint_of_z z :=
  match z with
   | Z0 => bigint_zero
   | Zpos p => bigint_of_pos p
   | Zneg p => bigint_opp (bigint_of_pos p)
  end.
 
-Fixpoint bigint_of_n n :=
+Definition bigint_of_n n :=
  match n with
   | N0 => bigint_zero
   | Npos p => bigint_of_pos p
diff --git a/theories/extraction/ExtrOcamlIntConv.v b/theories/extraction/ExtrOcamlIntConv.v
index a5be08ece4..d9c88defa5 100644
--- a/theories/extraction/ExtrOcamlIntConv.v
+++ b/theories/extraction/ExtrOcamlIntConv.v
@@ -42,14 +42,14 @@ Fixpoint int_of_pos p :=
   | xI p => int_succ (int_twice (int_of_pos p))
  end.
 
-Fixpoint int_of_z z :=
+Definition int_of_z z :=
  match z with
   | Z0 => int_zero
   | Zpos p => int_of_pos p
   | Zneg p => int_opp (int_of_pos p)
  end.
 
-Fixpoint int_of_n n :=
+Definition int_of_n n :=
  match n with
   | N0 => int_zero
   | Npos p => int_of_pos p