Factorisation des types dans l'affichage des paramètres des (Co)Inductif/Record

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9918 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 16 insertions, 0 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index a67de715a..d859c7980 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -533,6 +533,22 @@ 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
+  | (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 []
+
 (**********************************************************************)
 (* Module substitution: relies on detyping                            *)