diff options
Diffstat (limited to 'kernel/byterun/coq_values.h')
| -rw-r--r-- | kernel/byterun/coq_values.h | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index a186d62a..a5176f3f 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -14,15 +14,25 @@ #include "alloc.h" #include "mlvalues.h" +#define Default_tag 0 +#define Accu_tag 0 + + + +#define ATOM_ID_TAG 0 +#define ATOM_IDDEF_TAG 1 +#define ATOM_INDUCTIVE_TAG 2 #define ATOM_FIX_TAG 3 #define ATOM_SWITCH_TAG 4 +#define ATOM_COFIX_TAG 5 +#define ATOM_COFIXEVALUATED_TAG 6 + -#define Accu_tag 0 -#define Default_tag 0 /* Les blocs accumulate */ #define Is_accu(v) (Is_block(v) && (Tag_val(v) == Accu_tag)) +#define IS_EVALUATED_COFIX(v) (Is_accu(v) && Is_block(Field(v,1)) && (Tag_val(Field(v,1)) == ATOM_COFIXEVALUATED_TAG)) #endif /* _COQ_VALUES_ */ |