From 5b0769b33004202d015770aff3f3cdd347b099fb Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 10 Oct 2014 03:45:03 -0400 Subject: Fix segfault in native compiler on int31 division. Thanks to Yves for reporting it! --- kernel/retroknowledge.ml | 1 + kernel/retroknowledge.mli | 1 + 2 files changed, 2 insertions(+) (limited to 'kernel') diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index b645e256f1..8b451e2b8f 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -57,6 +57,7 @@ type int31_field = | Int31TimesC | Int31Div21 | Int31Div + | Int31Diveucl | Int31AddMulDiv | Int31Compare | Int31Head0 diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 846f135e6b..dde522e147 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -49,6 +49,7 @@ type int31_field = | Int31TimesC | Int31Div21 | Int31Div + | Int31Diveucl | Int31AddMulDiv | Int31Compare | Int31Head0 -- cgit v1.2.3