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 | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch) | |
tree | 591e9e512063e34099782e2518573f15ffeac003 /kernel/byterun/coq_values.h | |
parent | de0085539583f59dc7c4bf4e272e18711d565466 (diff) |
Imported Upstream version 8.1~gammaupstream/8.1.gamma
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_ */ |