diff options
| author | Maxime Dénès | 2014-10-10 03:45:03 -0400 |
|---|---|---|
| committer | Maxime Dénès | 2014-10-10 03:49:50 -0400 |
| commit | 5b0769b33004202d015770aff3f3cdd347b099fb (patch) | |
| tree | e3964c2163d73fbda3fd57be683f6e1c821e23e4 /tactics | |
| parent | ba50753e9da60a23a40dedea59fb7f25e3ba4d15 (diff) | |
Fix segfault in native compiler on int31 division.
Thanks to Yves for reporting it!
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/extraargs.ml4 | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index a4db321444..e129823f4c 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -285,6 +285,7 @@ PRINTED BY pr_r_int31_field | [ "int31" "timesc" ] -> [ Retroknowledge.Int31TimesC ] | [ "int31" "div21" ] -> [ Retroknowledge.Int31Div21 ] | [ "int31" "div" ] -> [ Retroknowledge.Int31Div ] +| [ "int31" "diveucl" ] -> [ Retroknowledge.Int31Diveucl ] | [ "int31" "addmuldiv" ] -> [ Retroknowledge.Int31AddMulDiv ] | [ "int31" "compare" ] -> [ Retroknowledge.Int31Compare ] | [ "int31" "head0" ] -> [ Retroknowledge.Int31Head0 ] |