diff options
Diffstat (limited to 'kernel/nativevalues.ml')
| -rw-r--r-- | kernel/nativevalues.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 51bf4c273..56dac4ecd 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -54,7 +54,8 @@ type atom = | Asort of sorts | Avar of identifier | Acase of annot_sw * accumulator * t * (t -> t) - | Afix of t array * t array * rec_pos * int + | Afix of t array * t array * rec_pos * int + (* types, bodies, rec_pos, pos *) | Acofix of t array * t array * int * t | Acofixe of t array * t array * int * t | Aprod of name * t * (t -> t) |