From 7142034ac3e4d3919d2c1a01df960b79dad70151 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Wed, 31 Oct 2018 14:04:19 +0000
Subject: [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.
---
 test-suite/bugs/closed/bug_8885.v | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_8885.v

(limited to 'test-suite')

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).
-- 
cgit v1.2.3