Separation entre les 2 propositions de syntaxe

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

2 files changed, 25 insertions, 6 deletions

diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index ec608af6f4..1ba590cee5 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -349,6 +349,16 @@ let rec strip_domains (nal,ty) c =
           (bnd::bl, rest, c2)
         with Failure _ -> ([bnd],Some (nal,ty), c1))
 
+(* Re-share binders *)
+let rec factorize_binders = function
+  | ([] | [_] as l) -> l
+  | (nal,ty)::((nal',ty')::l as l') ->
+      try
+	let _ = check_same_type ty ty' in
+	factorize_binders ((nal@nal',ty)::l)
+      with _ ->
+	(nal,ty) :: factorize_binders l'
+
 let rec extract_def_binders c ty =
   match c with
     | CLambdaN(loc,bvar::lams,b) ->
@@ -360,7 +370,7 @@ let rec extract_def_binders c ty =
               | None, _ -> CLambdaN(loc,lams,b)
               | Some bvar,_ -> CLambdaN(loc,bvar::lams,b) in
           let (bl,c2,ty2) = extract_def_binders c' ty' in
-          (bvar'@bl, c2, ty2)
+          (factorize_binders (bvar'@bl), c2, ty2)
         with Failure _ ->
           ([],c,ty))
     | _ -> ([],c,ty)
@@ -403,6 +413,11 @@ let pr_annotation pr po =
       None -> mt()
     | Some p -> spc() ++ str "=> " ++ hov 0 (pr ltop p)
 
+let pr_annotation2 pr po =
+  match po with
+      None -> mt()
+    | Some p -> spc() ++ str "of type " ++ hov 0 (pr ltop p)
+
 let rec pr inherited a =
   let (strm,prec) = match a with
   | CRef r -> pr_reference r, latom
@@ -447,9 +462,12 @@ let rec pr inherited a =
   | CCases (_,po,c,eqns) ->
       v 0
         (hov 4 (str "match " ++ prlist_with_sep sep_v (pr ltop) c ++
-                str " with") ++
+	(if !Options.p1 then pr_annotation pr po else mt ()) ++
+	str " with") ++
         prlist (pr_eqn pr) eqns ++
-        spc() ++ pr_annotation pr po ++ str "end"),
+	(if !Options.p1 then mt () else pr_annotation2 pr po)
+	++ spc() ++ 
+	str "end"),
       latom
   | COrderedCase (_,_,po,c,[b1;b2]) ->
       (* On force les parenthèses autour d'un "if" sous-terme (même si le
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 153f38d91b..e0e2c4a654 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -256,9 +256,9 @@ let pr_binder pr_c ty na =
         (surround_binder (pr_located pr_name na ++ str":" ++ cut() ++ pr_c ty))
 
 let pr_valdecls pr_c = function
-  | LocalRawAssum (na,c) ->
+  | LocalRawAssum (nal,c) ->
       let sep = if !Options.p1 then spc else pr_tight_coma in
-      prlist_with_sep sep (pr_binder pr_c c) na
+      prlist_with_sep sep (pr_binder pr_c c) nal
   | LocalRawDef (na,c) ->
       hov 1
         (surround_binder (pr_located pr_name na ++ str":=" ++ cut() ++ pr_c c))
@@ -708,7 +708,8 @@ let rec pr_vernac = function
 
   (* Solving *)
   | VernacSolve (i,tac,deftac) ->
-      (if i = 1 then mt() else int i ++ str ": ") ++ str "By " ++
+      (if i = 1 then mt() else int i ++ str ": ") ++
+      (if !Options.p1 then mt () else str "By ") ++
       (if deftac then mt() else str "!! ") ++
       pr_raw_tactic_goal i tac
   | VernacSolveExistential (i,c) ->