From 9afd34a59fe6d7e4551f1e1e5c7d051ae9da2199 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 30 Jun 2007 11:33:15 +0000
Subject: Correction bug sur factorisation affichage paramètres (cf r9918)

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

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index d859c79800..21ea677579 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -533,21 +533,21 @@ and detype_binder isgoal bk avoid env na ty c =
   | BLambda -> RLambda (dl, na',detype isgoal avoid env ty, r)
   | BLetIn -> RLetIn (dl, na',detype isgoal avoid env ty, r)
 
-let rec detype_rel_context where avoid env = 
-  let rec aux avoid env sign = function
-  | [] -> sign
+let rec detype_rel_context where avoid env sign =
+  let where = option_map (fun c -> it_mkLambda_or_LetIn c sign) where in
+  let rec aux avoid env = function
+  | [] -> []
   | (na,b,t)::rest ->
       let na',avoid' =
 	match where with
 	| None -> na,avoid
 	| Some c ->
-	    let c = it_mkLambda_or_LetIn c rest in
 	    if b<>None then concrete_let_name None avoid env na c
 	    else concrete_name None avoid env na c in
       let b = option_map (detype false avoid env) b in
       let t = detype false avoid env t in
-      aux avoid' (add_name na' env) ((na',b,t)::sign) rest
-  in aux avoid env []
+      (na',b,t) :: aux avoid' (add_name na' env) rest
+  in aux avoid env (List.rev sign)
 
 (**********************************************************************)
 (* Module substitution: relies on detyping                            *)
-- 
cgit v1.2.3