diff options
| author | Matthieu Sozeau | 2013-12-17 16:12:50 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2013-12-17 16:12:50 +0100 |
| commit | 35e47b6be8d9e97b58464daccc28d179951b5e47 (patch) | |
| tree | 09fd0f336e1fdd774ebbcd41d2849dfb54c76cb9 /kernel/reduction.mli | |
| parent | fb59652405d0e6a9d1100142d473374cd82ae16b (diff) | |
Tentative fix of the guardedness checker by Christine and me. All stdlib and test-suite pass.
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 3f958dc9d9..6e4634194d 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 |