Porting guard fix to checker.

1 files changed, 16 insertions, 0 deletions

diff --git a/checker/reduction.ml b/checker/reduction.ml
index 289b9a758..7bdc96283 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -499,6 +499,22 @@ let dest_prod_assum env =
   in
   prodec_rec env empty_rel_context
 
+let dest_lam_assum env =
+  let rec lamec_rec env l ty =
+    let rty = whd_betadeltaiota_nolet env ty in
+    match rty with
+    | Lambda (x,t,c)  ->
+        let d = (x,None,t) in
+	lamec_rec (push_rel d env) (d::l) c
+    | LetIn (x,b,t,c) ->
+        let d = (x,Some b,t) in
+	lamec_rec (push_rel d env) (d::l) c
+    | Cast (c,_,_)    -> lamec_rec env l c
+    | _               -> l,rty
+  in
+  lamec_rec env empty_rel_context
+
+
 let dest_arity env c =
   let l, c = dest_prod_assum env c in
   match c with