From 35e47b6be8d9e97b58464daccc28d179951b5e47 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 17 Dec 2013 16:12:50 +0100 Subject: Tentative fix of the guardedness checker by Christine and me. All stdlib and test-suite pass. --- kernel/reduction.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'kernel/reduction.mli') 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 -- cgit v1.2.3