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

There was also a non truly recursive in the doc.

1 files changed, 1 insertions, 1 deletions

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