diff options
Diffstat (limited to 'kernel/nativevalues.mli')
-rw-r--r-- | kernel/nativevalues.mli | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index c8adb07e5..150811b72 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -50,6 +50,8 @@ type atom = | Acofix of t array * t array * int * t | Acofixe of t array * t array * int * t | Aprod of name * t * (t -> t) + | Ameta of metavariable * t + | Aevar of existential * t (* Constructors *) @@ -63,7 +65,9 @@ val mk_var_accu : identifier -> t val mk_sw_accu : annot_sw -> accumulator -> t -> (t -> t) val mk_prod_accu : name -> t -> t -> t val mk_fix_accu : rec_pos -> int -> t array -> t array -> t -val mk_cofix_accu : int -> t array -> t array -> t +val mk_cofix_accu : int -> t array -> t array -> t +val mk_meta_accu : metavariable -> t +val mk_evar_accu : existential -> t -> t val upd_cofix : t -> t -> unit val force_cofix : t -> t val mk_const : tag -> t |