diff options
Diffstat (limited to 'kernel/byterun/coq_values.h')
| -rw-r--r-- | kernel/byterun/coq_values.h | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h new file mode 100644 index 00000000..a186d62a --- /dev/null +++ b/kernel/byterun/coq_values.h @@ -0,0 +1,28 @@ +/***********************************************************************/ +/* */ +/* Coq Compiler */ +/* */ +/* Benjamin Gregoire, projets Logical and Cristal */ +/* INRIA Rocquencourt */ +/* */ +/* */ +/***********************************************************************/ + +#ifndef _COQ_VALUES_ +#define _COQ_VALUES_ + +#include "alloc.h" +#include "mlvalues.h" + +#define ATOM_FIX_TAG 3 +#define ATOM_SWITCH_TAG 4 + +#define Accu_tag 0 +#define Default_tag 0 + +/* Les blocs accumulate */ +#define Is_accu(v) (Is_block(v) && (Tag_val(v) == Accu_tag)) + +#endif /* _COQ_VALUES_ */ + + |