diff options
Diffstat (limited to 'kernel/byterun/coq_values.h')
| -rw-r--r-- | kernel/byterun/coq_values.h | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index f07018711b..0cdef34050 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -30,9 +30,6 @@ #define Is_double(v) (Tag_val(v) == Double_tag) #define Is_tailrec_switch(v) (Field(v,1) == Val_true) -/* coq array */ -#define Is_coq_array(v) (Is_block(v) && (Wosize_val(v) == 1)) - /* coq values for primitive operations */ #define coq_tag_C1 2 #define coq_tag_C0 1 |