diff options
Diffstat (limited to 'kernel/nativelambda.mli')
| -rw-r--r-- | kernel/nativelambda.mli | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index 093665df9b..446df1a1ea 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -34,8 +34,8 @@ type lambda = | Lfix of (int array * (string * inductive) array * int) * fix_decl | Lcofix of int * fix_decl | Lint of int (* a constant constructor *) - | Lmakeblock of prefix * constructor * int * lambda array - (* prefix, constructor Name.t, constructor tag, arguments *) + | Lmakeblock of prefix * inductive * int * lambda array + (* prefix, inductive name, constructor tag, arguments *) (* A fully applied non-constant constructor *) | Luint of Uint63.t | Lval of Nativevalues.t @@ -44,7 +44,10 @@ type lambda = | Llazy | Lforce -and lam_branches = (constructor * Name.t Context.binder_annot array * lambda) array +and lam_branches = + { constant_branches : lambda array; + nonconstant_branches : (Name.t Context.binder_annot array * lambda) array; + } and fix_decl = Name.t Context.binder_annot array * lambda array * lambda array |