modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixes

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

2 files changed, 20 insertions, 15 deletions

diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 74914503f..4c5821dcc 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -277,7 +277,7 @@ let rec factorize_binders = function
 	d :: factorize_binders l')
   | d :: l -> d :: factorize_binders l
 
-(* Extrac lambdas when a type constraint occurs *)
+(* Extract lambdas when a type constraint occurs *)
 let rec extract_def_binders c ty =
   match c with
     | CLambdaN(loc,bvar::lams,b) ->
@@ -302,8 +302,10 @@ let rec split_fix n typ def =
     let (bl,typ,def) = split_fix (n-1) typ def in
     (LocalRawAssum ([na],t)::bl,typ,def)
 
-let pr_recursive_decl pr id b t c =
-  pr_id id ++ b ++ pr_opt_type_spc pr t ++ str " :=" ++
+let pr_recursive_decl pr id bl annot t c =
+  pr_id id ++ str" " ++
+  hov 0 (pr_undelimited_binders (pr ltop) bl ++ annot) ++
+  pr_opt_type_spc pr t ++ str " :=" ++
   brk(1,2) ++ pr ltop c
 
 let name_of_binder = function
@@ -311,19 +313,20 @@ let name_of_binder = function
   | LocalRawDef (_,_) -> []
 
 let pr_fixdecl pr (id,n,t0,c0) =
-  let (bl,t,c) = extract_def_binders t0 c0 in
+  let (bl,c,t) = extract_def_binders c0 t0 in
   let (bl,t,c) =
-    if List.length bl <= n then split_fix (n+1) t0 c0 else (bl,t,c) in
+    let ids = List.flatten (List.map name_of_binder bl) in
+    if List.length ids <= n then split_fix (n+1) t0 c0 else (bl,t,c) in
   let annot =
     let ids = List.flatten (List.map name_of_binder bl) in
     if List.length ids > 1 then 
-      spc() ++ str "{struct " ++ pr_name (snd (list_last ids)) ++ str"}"
+      spc() ++ str "{struct " ++ pr_name (snd (List.nth ids n)) ++ str"}"
     else mt() in
-  pr_recursive_decl pr id
-    (str" " ++ hov 0 (pr_undelimited_binders (pr ltop) bl) ++ annot) t c
+  pr_recursive_decl pr id bl annot t c
 
 let pr_cofixdecl pr (id,t,c) =
-  pr_recursive_decl pr id (mt ()) t c
+  let (bl,c,t) = extract_def_binders c t in
+  pr_recursive_decl pr id bl (mt()) t c
 
 let pr_recursive pr_decl id = function
   | [] -> anomaly "(co)fixpoint with no definition"
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index 5fce8607d..0501319a8 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -184,11 +184,13 @@ let pr_esubst prc l =
 
 let pr_bindings_gen for_ex prlc prc = function
   | ImplicitBindings l ->
-      spc () ++ (if for_ex then mt() else str "with" ++ spc ()) ++
-      hv 0 (prlist_with_sep spc prc l)
+      spc () ++
+      hv 2 ((if for_ex then mt() else str "with" ++ spc ()) ++
+            prlist_with_sep spc prc l)
   | ExplicitBindings l ->
-      spc () ++ (if for_ex then mt() else str "with" ++ spc ()) ++
-      hv 0 (pr_esubst prlc l)
+      spc () ++
+      hv 2 ((if for_ex then mt() else str "with" ++ spc ()) ++
+            pr_esubst prlc l)
   | NoBindings -> mt ()
 
 let pr_bindings prlc prc = pr_bindings_gen false prlc prc
@@ -197,9 +199,9 @@ let pr_with_bindings prlc prc (c,bl) =
   if Options.do_translate () then
     (* translator calls pr_with_bindings on rawconstr: we cast it! *)
     let bl' = translate_with_bindings (fst (Obj.magic c) : rawconstr) bl in
-    prc c ++ pr_bindings prlc prc bl'
+    hov 1 (prc c ++ pr_bindings prlc prc bl')
   else
-    prc c ++ pr_bindings prlc prc bl
+    hov 1 (prc c ++ pr_bindings prlc prc bl)
 
 let pr_with_constr prc = function
   | None -> mt ()