diff options
| author | Vincent Laporte | 2018-10-31 14:04:19 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2018-11-08 10:48:23 +0000 |
| commit | 7142034ac3e4d3919d2c1a01df960b79dad70151 (patch) | |
| tree | dca9661ad251dfa6feaa62172b2b41c1f1cefe2e /test-suite | |
| parent | c4880effb91fab55c250a799cbceac9b04681db0 (diff) | |
[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.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_8885.v | 8 |
1 files changed, 8 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). |