diff options
| author | letouzey | 2012-08-11 13:33:26 +0000 |
|---|---|---|
| committer | letouzey | 2012-08-11 13:33:26 +0000 |
| commit | 5c825f263698433ed4e8db8ccd0c14394520535a (patch) | |
| tree | a9855a96d5e780166652b93376fea2483f9863c4 /kernel/cbytecodes.ml | |
| parent | c02c86626e36c908ec76854f8eda2d5278141d12 (diff) | |
fast bitwise operations (lor,land,lxor) on int31 and BigN
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15727 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/cbytecodes.ml')
| -rw-r--r-- | kernel/cbytecodes.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index c0119aa26b..994242a8a4 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -114,6 +114,9 @@ type instruction = | Kareconst of int*Label.t (* conditional jump *) | Kcompint31 (* dynamic compilation of int31 *) | Kdecompint31 (* dynamic decompilation of int31 *) + | Klorint31 (* bitwise operations: or and xor *) + | Klandint31 + | Klxorint31 (* /spiwack *) and bytecodes = instruction list @@ -220,6 +223,9 @@ let rec instruction ppf = function | Kareconst(n,lbl) -> fprintf ppf "\tareconst %i %i" n lbl | Kcompint31 -> fprintf ppf "\tcompint31" | Kdecompint31 -> fprintf ppf "\tdecompint" + | Klorint31 -> fprintf ppf "\tlorint31" + | Klandint31 -> fprintf ppf "\tlandint31" + | Klxorint31 -> fprintf ppf "\tlxorint31" (* /spiwack *) |