diff options
Diffstat (limited to 'kernel/nativevalues.ml')
| -rw-r--r-- | kernel/nativevalues.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 043f06e26..d88d5d25d 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -60,6 +60,7 @@ type atom = | Aprod of name * t * (t -> t) | Ameta of metavariable * t | Aevar of existential * t + | Aproj of constant * accumulator let accumulate_tag = 0 @@ -128,6 +129,9 @@ let mk_meta_accu mv ty = let mk_evar_accu ev ty = mk_accu (Aevar (ev,ty)) +let mk_proj_accu kn c = + mk_accu (Aproj (kn,c)) + let atom_of_accu (k:accumulator) = (Obj.magic (Obj.field (Obj.magic k) 2) : atom) |