diff options
Diffstat (limited to 'kernel/byterun/coq_values.h')
| -rw-r--r-- | kernel/byterun/coq_values.h | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index 48fba64bf..a5176f3f5 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -32,6 +32,7 @@ /* 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_ */ |