From 32c900252a07ea7d2dd9fe15feb21ef98aee3df7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 25 Nov 2013 14:14:54 +0100
Subject: Typo resulting in bad eta-expansion of destructing let's body.
 Revealed by message on coq-club on 24/11/2013.

---
 pretyping/detyping.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index bdbfe412e7..4e0fc5de69 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -305,7 +305,7 @@ let it_destRLambda_or_LetIn_names n c =
 	  let a = GVar (dl,x) in
 	  aux (n-1) (Name x :: nal)
             (match c with
-              | GApp (loc,p,l) -> GApp (loc,c,l@[a])
+              | GApp (loc,p,l) -> GApp (loc,p,l@[a])
               | _ -> (GApp (dl,c,[a])))
   in aux n [] c
 
-- 
cgit v1.2.3