diff options
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 3f958dc9d..6e4634194 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -79,6 +79,7 @@ val hnf_prod_applist : env -> types -> constr list -> types val dest_prod : env -> types -> rel_context * types val dest_prod_assum : env -> types -> rel_context * types +val dest_lam_assum : env -> types -> rel_context * types exception NotArity |