From 008253465b65c0c50477bf830bab3590564706a4 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 27 Jun 2004 19:06:36 +0000
Subject: Correction affichage v8 des records avec let (bug #798)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5830 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/detyping.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 9666008c39..203dd4db3e 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -277,10 +277,10 @@ let detype_case computable detype detype_eqn testdep
       let rec decomp_lam_force n avoid l p =
 	if n = 0 then (List.rev l,p) else
           match p with
-            | RLambda (_,(Name id as na),_,c) -> 
-		decomp_lam_force (n-1) (id::avoid) (na::l) c
-            | RLambda (_,(Anonymous as na),_,c) -> 
-		decomp_lam_force (n-1) avoid (na::l) c
+            | RLambda (_,na,_,c) -> 
+		decomp_lam_force (n-1) (name_cons na avoid) (na::l) c
+            | RLetIn (_,na,_,c) -> 
+		decomp_lam_force (n-1) (name_cons na avoid) (na::l) c
             | _ ->
 		let x = Nameops.next_ident_away (id_of_string "x") avoid in
 		decomp_lam_force (n-1) (x::avoid) (Name x :: l) 
-- 
cgit v1.2.3