From aa63497700bb2e75767c1891a961fc06ba329065 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 22 Jul 2014 15:57:27 -0400 Subject: Porting guard fix to checker. --- checker/reduction.mli | 2 ++ 1 file changed, 2 insertions(+) (limited to 'checker/reduction.mli') diff --git a/checker/reduction.mli b/checker/reduction.mli index 915805d26..4b64f9af7 100644 --- a/checker/reduction.mli +++ b/checker/reduction.mli @@ -47,5 +47,7 @@ val hnf_prod_applist : env -> constr -> constr list -> constr val dest_prod : env -> constr -> rel_context * constr val dest_prod_assum : env -> constr -> rel_context * constr +val dest_lam_assum : env -> constr -> rel_context * constr + val dest_arity : env -> constr -> arity -- cgit v1.2.3