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

6 files changed, 27 insertions, 14 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index cf4d2db0e4..37e47301ac 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -992,3 +992,8 @@ and raw_of_eqn env constr construct_nargs branch =
 
 let extern_constr_pattern env pat =
   extern true (None,[]) Idset.empty (raw_of_pat env pat)
+
+let extern_rel_context where env sign =
+  let a = detype_rel_context where [] (names_of_rel_context env) sign in
+  let vars = vars_of_env env in
+  snd (extern_local_binder (None,[]) vars a)
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index a0f8661ccd..7ae2977f5c 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -42,6 +42,8 @@ val extern_constr_in_scope : bool -> scope_name -> env -> constr -> constr_expr
 val extern_reference : loc -> Idset.t -> global_reference -> reference
 val extern_type : bool -> env -> types -> constr_expr
 val extern_sort : sorts -> rawsort
+val extern_rel_context : constr option -> env -> 
+  rel_context -> local_binder list
 
 (* Printing options *)
 val print_implicits : bool ref
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index f0a44311bc..65439dd268 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -233,10 +233,6 @@ let pr_delimited_binders kw pr_c bl =
       pr_com_at n ++ kw() ++ pr_undelimited_binders pr_c bdl
   | _ -> assert false
 
-let pr_let_binder pr x a =
-  hov 0 (hov 0 (pr_name x ++ brk(0,1) ++ str ":=") ++
-         pr_sep_com (fun () -> brk(0,1)) (pr ltop) a)
-
 let rec extract_prod_binders = function
 (*  | CLetIn (loc,na,b,c) as x ->
       let bl,c = extract_prod_binders c in
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 4619e50ec7..dc7552fcd1 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -171,15 +171,7 @@ let pr_named_context env ne_context =
           ne_context ~init:(mt ()))
 
 let pr_rel_context env rel_context =
-  let rec prec env = function
-    | [] -> (mt ()) 
-    | [b] -> str "(" ++ pr_rel_decl env b ++ str")"
-    | b::rest ->
-        let pb = pr_rel_decl env b in
-        let penvtl = prec (push_rel b env) rest in
-        str "(" ++ pb ++ str")" ++ spc () ++ penvtl
-  in 
-  hov 0 (prec env (List.rev rel_context))
+  pr_binders (extern_rel_context None env rel_context)
 
 let pr_rel_context_of env =
   pr_rel_context env (rel_context env)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index a67de715a8..d859c79800 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                            *)
 
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 0e9166ac4c..445c2183df 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -40,6 +40,9 @@ val detype_case :
 
 val detype_sort : sorts -> rawsort
 
+val detype_rel_context : constr option -> identifier list -> names_context ->
+  rel_context -> (name * rawconstr option * rawconstr) list
+
 (* look for the index of a named var or a nondep var as it is renamed *)
 val lookup_name_as_renamed  : env -> constr -> identifier -> int option
 val lookup_index_as_renamed : env -> constr -> int -> int option
@@ -57,4 +60,3 @@ val simple_cases_matrix_of_branches :
   inductive -> int list -> rawconstr list -> cases_clauses
 val return_type_of_predicate :
   inductive -> int -> int -> rawconstr -> predicate_pattern * rawconstr option
-