diff options
| author | Pierre-Marie Pédrot | 2015-10-12 18:54:31 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-12 18:54:31 +0200 |
| commit | 10e5883fed21f9631e1aa65adb7a7e62a529987f (patch) | |
| tree | f04cfc472e6345585eb5f606e2957fcf0f2740ea /kernel/cbytecodes.ml | |
| parent | 75c5e421e91d49eec9cd55c222595d2ef45325d6 (diff) | |
| parent | 26974a4a2301cc7b1188a3f2f29f3d3368eccc0b (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'kernel/cbytecodes.ml')
| -rw-r--r-- | kernel/cbytecodes.ml | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 891d95378b..448bf85444 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -17,13 +17,16 @@ open Term type tag = int -let id_tag = 0 -let iddef_tag = 1 -let ind_tag = 2 -let fix_tag = 3 +let accu_tag = 0 + +let max_atom_tag = 1 +let proj_tag = 2 +let fix_app_tag = 3 let switch_tag = 4 let cofix_tag = 5 let cofix_evaluated_tag = 6 + + (* It would be great if OCaml exported this value, So fixme if this happens in a new version of OCaml *) let last_variant_tag = 245 |