diff options
| author |  bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-06-20 09:43:36 +0000 |
|---|---|---|
| committer | bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-06-20 09:43:36 +0000 |
| commit | f4586d1e8b1116340574d9660117f93e7a1e4e3b (patch) | |
| tree | 15b7dff4ed22b762446e4ae1f426e8f8aa2de52c /kernel/cbytecodes.ml | |
| parent | 4708506ca1b34e93835b163db102f6860c89190c (diff) | |
ajout de head0 et tail0 en natif
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9900 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/cbytecodes.ml')
| -rw-r--r-- | kernel/cbytecodes.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index ee8cb1eea..84d04d67e 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -89,10 +89,13 @@ type instruction = | Kaddmuldivint31 (* generic operation for shifting and cycling. Takes 3 int31 i j and s, and returns x*2^s+y/(2^(31-s) *) - | Kcompareint31 (* unsigned comparison of int31 + | Kcompareint31 (* unsigned comparison of int31 cf COMPAREINT31 in kernel/byterun/coq_interp.c for more info *) + | Khead0int31 (* Give the numbers of 0 in head of a in31*) + | Ktail0int31 (* Give the numbers of 0 in tail of a in31 + ie low bits *) | Kisconst of Label.t (* conditional jump *) | Kareconst of int*Label.t (* conditional jump *) | Kcompint31 (* dynamic compilation of int31 *) @@ -196,6 +199,8 @@ let rec instruction ppf = function | Kdiv21int31 -> fprintf ppf "\tdiv21int31" | Kdivint31 -> fprintf ppf "\tdivint31" | Kcompareint31 -> fprintf ppf "\tcompareint31" + | Khead0int31 -> fprintf ppf "\thead0int31" + | Ktail0int31 -> fprintf ppf "\ttail0int31" | Kaddmuldivint31 -> fprintf ppf "\taddmuldivint31" | Kisconst lbl -> fprintf ppf "\tisconst %i" lbl | Kareconst(n,lbl) -> fprintf ppf "\tareconst %i %i" n lbl |