diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
| commit | 70b9be8acc1d1ada178a95c1cd4013506e9d0d1b (patch) | |
| tree | f672a286d962cc67c95874b3b60402fc957870b6 /kernel/byterun/coq_values.h | |
| parent | a5bd4e097a94cc4f863bf4d4bcc5ce592c30ba47 (diff) | |
| parent | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (diff) | |
Merge commit 'upstream/8.1.gamma' into 8.1
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_ */ |