From c88f47195955beb615d15dd9d57e4de20e5e3a52 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 10 Jul 2014 10:31:59 +0200
Subject: Reduce non-toplevel letins in splay_prod_assum (bug found in Ergo).

---
 pretyping/reductionops.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index c9d4e388d6..f4b32ee779 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1375,7 +1375,10 @@ let splay_prod_assum env sigma =
 	prodec_rec (push_rel (x, Some b, t) env)
 	  (add_rel_decl (x, Some b, t) l) c
     | Cast (c,_,_)    -> prodec_rec env l c
-    | _               -> l,t
+    | _               -> 
+      let t' = whd_betadeltaiota env sigma t in
+	if Term.eq_constr t t' then l,t
+	else prodec_rec env l t'
   in
   prodec_rec env empty_rel_context
 
-- 
cgit v1.2.3