[VM] Fix compilation of int31 eliminators

The compilation to bytecode of the elimination schemes for int31 must
happen after the int31 type is registered to the retroknowledge.
Otherwise, the “decompint” instruction is not emitted.

2 files changed, 14 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_8885.v b/test-suite/bugs/closed/bug_8885.v
new file mode 100644
index 0000000000..9d86c08d71
--- /dev/null
+++ b/test-suite/bugs/closed/bug_8885.v
@@ -0,0 +1,8 @@
+From Coq Require Import Cyclic31.
+
+Definition Nat `(int31) := nat.
+Definition Zero (_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _: digits) := 0.
+
+Check (eq_refl (int31_rect Nat Zero 1) : 0 = 0).
+Check (eq_refl (int31_rect Nat Zero 1) <: 0 = 0).
+Check (eq_refl (int31_rect Nat Zero 1) <<: 0 = 0).
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index 3a2503d6b7..ce540775e3 100644
--- a/theories/Numbers/Cyclic/Int31/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
@@ -15,6 +15,8 @@ Require Import Wf_nat.
 Require Export ZArith.
 Require Export DoubleType.
 
+Local Unset Elimination Schemes.
+
 (** * 31-bit integers *)
 
 (** This file contains basic definitions of a 31-bit integer
@@ -48,6 +50,10 @@ Inductive int31 : Type := I31 : digits31 int31.
 Register digits as int31.bits.
 Register int31 as int31.type.
 
+Scheme int31_ind := Induction for int31 Sort Prop.
+Scheme int31_rec := Induction for int31 Sort Set.
+Scheme int31_rect := Induction for int31 Sort Type.
+
 Declare Scope int31_scope.
 Declare ML Module "int31_syntax_plugin".
 Delimit Scope int31_scope with int31.