From b44b68ec704df75f684e3393980f3518caf1a506 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sun, 6 Jul 2014 20:08:06 +0200
Subject: In dest_prod_assum, allow non-toplevel let-reductions (fixes a bug
 found in MathClasses).

---
 kernel/reduction.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 1e6f157ab5..a4d8872fed 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -758,7 +758,7 @@ let dest_prod env =
   in
   decrec env empty_rel_context
 
-(* The same but preserving lets *)
+(* The same but preserving lets in the context, not internal ones. *)
 let dest_prod_assum env =
   let rec prodec_rec env l ty =
     let rty = whd_betadeltaiota_nolet env ty in
@@ -770,7 +770,10 @@ let dest_prod_assum env =
         let d = (x,Some b,t) in
 	prodec_rec (push_rel d env) (add_rel_decl d l) c
     | Cast (c,_,_)    -> prodec_rec env l c
-    | _               -> l,rty
+    | _               ->
+      let rty' = whd_betadeltaiota env rty in
+	if Term.eq_constr rty' rty then l, rty
+	else prodec_rec env l rty'
   in
   prodec_rec env empty_rel_context
 
-- 
cgit v1.2.3