From 08c9ac8e0919ed7e6c001542c2094640f1d7bd73 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Mon, 5 Aug 2019 08:28:49 +0000
Subject: ConstructiveCauchyReals: make explicit structural recursion

---
 theories/Reals/ConstructiveCauchyReals.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Reals/ConstructiveCauchyReals.v b/theories/Reals/ConstructiveCauchyReals.v
index 5a0f4abec7..3ca9248600 100644
--- a/theories/Reals/ConstructiveCauchyReals.v
+++ b/theories/Reals/ConstructiveCauchyReals.v
@@ -1144,7 +1144,7 @@ Proof.
   - intro abs. apply (CReal_plus_lt_compat_l r) in abs. contradiction.
 Qed.
 
-Fixpoint BoundFromZero (qn : nat -> Q) (k : nat) (A : positive)
+Fixpoint BoundFromZero (qn : nat -> Q) (k : nat) (A : positive) {struct k}
   : (forall n:nat, le k n -> Qlt (Qabs (qn n)) (Z.pos A # 1))
     -> { B : positive | forall n:nat, Qlt (Qabs (qn n)) (Z.pos B # 1) }.
 Proof.
-- 
cgit v1.2.3