Merge PR #12121: Fixes #11903 and warns about non truly-recursive (co)fixpoints

Ack-by: Zimmi48
Reviewed-by: ppedrot

2 files changed, 4 insertions, 4 deletions

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