meilleure presentation des commentaires du traducteur

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

4 files changed, 205 insertions, 142 deletions

diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 128cd148f7..8e71287153 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -23,7 +23,6 @@ open Term
 open Pattern
 (*i*)
 
-let sep = fun _ -> brk(1,0)
 let sep_p = fun _ -> str"."
 let sep_v = fun _ -> str"," ++ spc()
 let sep_pp = fun _ -> str":"
@@ -77,11 +76,28 @@ let pr_delimiters key strm =
 
 let surround p = str"(" ++ p ++ str")"
 
+let pr_located pr ((b,e),x) =
+  if Options.do_translate() && (b,e)<>dummy_loc then
+    comment b ++ pr x ++ comment e
+  else pr x
+
+let pr_com_at n =
+  if Options.do_translate() && n <> 0 then comment n 
+  else mt()
+
+let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp)
+
+let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c)
+
 open Rawterm
 
 let pr_opt pr = function
   | None -> mt ()
-  | Some x -> spc () ++ pr x
+  | Some x -> spc() ++ pr x
+
+let pr_optc pr = function
+  | None -> mt ()
+  | Some x -> pr_sep_com spc pr x
 
 let pr_universe u = str "<univ>"
 
@@ -93,9 +109,10 @@ let pr_sort = function
 let pr_expl_args pr (a,expl) =
   match expl with
   | None -> pr (lapp,L) a
-  | Some (_,ExplByPos n) -> str "@" ++ int n ++ str ":=" ++ pr (lapp,L) a
+  | Some (_,ExplByPos n) ->
+      anomaly("Explicitation by position not implemented")
   | Some (_,ExplByName id) -> 
-      str "(" ++ pr_id id ++ str ":=" ++ pr (lapp,L) a ++ str ")"
+      str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")"
 
 let pr_opt_type pr = function
   | CHole _ -> mt ()
@@ -103,55 +120,70 @@ let pr_opt_type pr = function
 
 let pr_opt_type_spc pr = function
   | CHole _ -> mt ()
-  | t ->  str " :" ++ brk(1,2) ++ pr ltop t
+  | t ->  str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t
 
 let pr_name = function
   | Anonymous -> str"_"
   | Name id -> pr_id (Constrextern.v7_to_v8_id id)
 
-let pr_located pr ((b,e),x) =
-  if Options.do_translate() then comment b ++ pr x ++ comment e
-  else pr x
+let pr_lident (b,_ as loc,id) =
+  if loc <> dummy_loc then
+    pr_located pr_id ((b,b+String.length(string_of_id id)),id)
+  else pr_id id
 
-let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp)
+let pr_lname = function
+    (loc,Name id) -> pr_lident (loc,id)
+  | lna -> pr_located pr_name lna
 
 let pr_or_var pr = function
   | Genarg.ArgArg x -> pr x
-  | Genarg.ArgVar (loc,s) -> pr_with_comments loc (pr_id s)
+  | Genarg.ArgVar (loc,s) -> pr_lident (loc,s)
 
 let las = lapp
 
-let rec pr_patt inh p =
+let rec pr_patt sep inh p =
   let (strm,prec) = match p with
   | CPatAlias (_,p,id) ->
-      pr_patt (las,E) p ++ str " as " ++ pr_id id, las
+      pr_patt mt (las,E) p ++ str " as " ++ pr_id id, las
   | CPatCstr (_,c,[]) -> pr_reference c, latom
   | CPatCstr (_,c,args) ->
-      pr_reference c ++ spc() ++
-      prlist_with_sep sep (pr_patt (lapp,L)) args, lapp
+      pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp
   | CPatAtom (_,None) -> str "_", latom
   | CPatAtom (_,Some r) -> pr_reference r, latom
   | CPatNotation (_,"( _ )",[p]) ->
-      str"("++ pr_patt (max_int,E) p ++ str")", latom
-  | CPatNotation (_,s,env) -> pr_notation pr_patt s env
+      pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom
+  | CPatNotation (_,s,env) -> pr_notation (pr_patt mt) s env
   | CPatNumeral (_,i) -> Bignat.pr_bigint i, latom
-  | CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt lsimple p), 1
+  | CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt mt lsimple p), 1
   in
   let loc = cases_pattern_loc p in
-  pr_with_comments loc (if prec_less prec inh then strm else surround strm)
+  pr_with_comments loc
+    (sep() ++ if prec_less prec inh then strm else surround strm)
+
+let pr_patt = pr_patt mt
+
 
 let pr_eqn pr (loc,pl,rhs) =
   spc() ++ hov 4
     (pr_with_comments loc
       (str "| " ++
       hov 0 (prlist_with_sep sep_v (pr_patt ltop) pl ++ str " =>") ++
-      spc() ++ pr ltop rhs))
+      pr_sep_com spc (pr ltop) rhs))
+
+let begin_of_binder = function
+    LocalRawDef(((b,_),_),_) -> b
+  | LocalRawAssum(((b,_),_)::_,_) -> b
+  | _ -> assert false
+
+let begin_of_binders = function
+  | b::_ -> begin_of_binder b
+  | _ -> 0
 
 let pr_binder many pr (nal,t) =
   match t with
-  | CHole _ -> prlist_with_sep sep (pr_located pr_name) nal
+  | CHole _ -> prlist_with_sep spc pr_lname nal
   | _ ->
-    let s = prlist_with_sep sep (pr_located pr_name) nal ++ str" : " ++ pr t in
+    let s = prlist_with_sep spc pr_lname nal ++ str" : " ++ pr t in
     hov 1 (if many then surround s else s)
 
 let pr_binder_among_many pr_c = function
@@ -162,19 +194,24 @@ let pr_binder_among_many pr_c = function
         | CCast(_,c,t) -> c, t
         | _ -> c, CHole dummy_loc in
       hov 1 (surround
-        (pr_located pr_name na ++ pr_opt_type pr_c topt ++
+        (pr_lname na ++ pr_opt_type pr_c topt ++
          str":=" ++ cut() ++ pr_c c))
 
 let pr_undelimited_binders pr_c =
-  prlist_with_sep sep (pr_binder_among_many pr_c)
+  prlist_with_sep spc (pr_binder_among_many pr_c)
 
-let pr_delimited_binders pr_c = function
-  | [LocalRawAssum (nal,t)] -> pr_binder false pr_c (nal,t)
-  | LocalRawAssum _ :: _ as bdl -> pr_undelimited_binders pr_c bdl
+let pr_delimited_binders kw pr_c bl =
+  let n = begin_of_binders bl in
+  match bl with
+  | [LocalRawAssum (nal,t)] ->
+      pr_com_at n ++ kw() ++ pr_binder false pr_c (nal,t)
+  | LocalRawAssum _ :: _ as bdl ->
+      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 ":=") ++ brk(0,1) ++ pr ltop 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 ->
@@ -306,7 +343,7 @@ 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
+  pr_sep_com (fun () -> brk(1,2)) (pr ltop) c
 
 let name_of_binder = function
   | LocalRawAssum (nal,_) -> nal
@@ -377,7 +414,8 @@ let pr_case_item pr (tm,(na,indnalopt)) =
 let pr_case_type pr po =
   match po with
     | None | Some (CHole _) -> mt()
-    | Some p -> spc() ++ hov 2 (str "return" ++ spc () ++ pr (lcast,E) p)
+    | Some p ->
+        spc() ++ hov 2 (str "return" ++ pr_sep_com spc (pr lsimple) p)
 
 let pr_return_type pr po = pr_case_type pr po
 
@@ -393,80 +431,85 @@ let pr_proj pr pr_app a f l =
 let pr_appexpl pr f l =
       hov 2 (
 	str "@" ++ pr_reference f ++
-	prlist (fun a -> spc () ++ pr (lapp,L) a) l)
+	prlist (pr_sep_com spc (pr (lapp,L))) l)
 
 let pr_app pr a l =
   hov 2 (
     pr (lapp,L) a  ++ 
     prlist (fun a -> spc () ++ pr_expl_args pr a) l)
 
-let rec pr inherited a =
+let rec pr sep inherited a =
   let (strm,prec) = match a with
   | CRef r -> pr_reference r, latom
   | CFix (_,id,fix) ->
-      let p = hov 0 (str"fix " ++ pr_recursive (pr_fixdecl pr) (snd id) fix) in
+      let p = hov 0 (str"fix " ++
+                pr_recursive (pr_fixdecl (pr mt)) (snd id) fix) in
       if List.length fix = 1 & prec_less (fst inherited) ltop
       then surround p, latom else p, lfix
   | CCoFix (_,id,cofix) ->
       let p =
         hov 0 (str "cofix " ++
-               pr_recursive (pr_cofixdecl pr) (snd id) cofix) in
+               pr_recursive (pr_cofixdecl (pr mt)) (snd id) cofix) in
       if List.length cofix = 1 & prec_less (fst inherited) ltop
       then surround p, latom else p, lfix
   | CArrow (_,a,b) ->
-      hov 0 (pr (larrow,L) a ++ str " ->" ++ brk(1,0) ++ pr (-larrow,E) b),
+      hov 0 (pr mt (larrow,L) a ++ str " ->" ++
+             pr (fun () ->brk(1,0)) (-larrow,E) b),
       larrow
   | CProdN _ ->
       let (bl,a) = extract_prod_binders a in
-      hov 2 (
-	str"forall" ++ spc() ++ pr_delimited_binders (pr ltop) bl ++
-        str "," ++ spc() ++ pr ltop a),
+      hov 0 (
+	hov 2 (pr_delimited_binders (fun () -> str"forall" ++ spc())
+                 (pr mt ltop) bl) ++
+        str "," ++ pr spc ltop a),
       lprod
   | CLambdaN _ ->
       let (bl,a) = extract_lam_binders a in
-      hov 2 (
-	str"fun" ++ spc() ++ pr_delimited_binders (pr ltop) bl ++
-        str " =>" ++ spc() ++ pr ltop a),
+      hov 0 (
+        hov 2 (pr_delimited_binders (fun () -> str"fun" ++ spc())
+                 (pr mt ltop) bl) ++
+
+        str " =>" ++ pr spc ltop a),
       llambda
   | CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), b)
       when x=x' ->
       hv 0 (
-        hov 2 (str "let " ++ pr ltop fx ++ str " in") ++
-        spc () ++ pr ltop b),
+        hov 2 (str "let " ++ pr mt ltop fx ++ str " in") ++
+        pr spc ltop b),
       lletin
   | CLetIn (_,x,a,b) ->
       hv 0 (
-        hov 2 (str "let " ++ pr_located pr_name x ++ str " :=" ++ spc() ++
-               pr ltop a ++ str " in") ++
-        spc () ++ pr ltop b),
+        hov 2 (str "let " ++ pr_lname x ++ str " :=" ++
+               pr spc ltop a ++ str " in") ++
+        pr spc ltop b),
       lletin
   | CAppExpl (_,(Some i,f),l) ->
       let l1,l2 = list_chop i l in
       let c,l1 = list_sep_last l1 in
-      let p = pr_proj pr pr_appexpl c f l1 in
+      let p = pr_proj (pr mt) pr_appexpl c f l1 in
       if l2<>[] then
-	p ++ prlist (fun a -> spc () ++ pr (lapp,L) a) l2, lapp
+	p ++ prlist (pr spc (lapp,L)) l2, lapp
       else
 	p, lproj
-  | CAppExpl (_,(None,f),l) -> pr_appexpl pr f l, lapp
+  | CAppExpl (_,(None,f),l) -> pr_appexpl (pr mt) f l, lapp
   | CApp (_,(Some i,f),l) ->
       let l1,l2 = list_chop i l in
       let c,l1 = list_sep_last l1 in
       assert (snd c = None);
-      let p = pr_proj pr pr_app (fst c) f l1 in
+      let p = pr_proj (pr mt) pr_app (fst c) f l1 in
       if l2<>[] then 
-	p ++ prlist (fun a -> spc () ++ pr_expl_args pr a) l2, lapp
+	p ++ prlist (fun a -> spc () ++ pr_expl_args (pr mt) a) l2, lapp
       else
 	p, lproj
-  | CApp (_,(None,a),l) -> pr_app pr a l, lapp
+  | CApp (_,(None,a),l) -> pr_app (pr mt) a l, lapp
   | CCases (_,(po,rtntypopt),c,eqns) ->
       v 0
         (hv 0 (str "match" ++ brk (1,2) ++
 	  hov 0 (
-	    prlist_with_sep sep_v (pr_case_item pr) c
-            ++ pr_case_type pr rtntypopt) ++
+	    prlist_with_sep sep_v (pr_case_item (pr mt)) c
+            ++ pr_case_type (pr mt) rtntypopt) ++
 	spc () ++ str "with") ++
-        prlist (pr_eqn pr) eqns ++ spc() ++ str "end"),
+        prlist (pr_eqn (pr mt)) eqns ++ spc() ++ str "end"),
       latom
   | CLetTuple (_,nal,(na,po),c,b) ->
       hv 0 (
@@ -474,27 +517,28 @@ let rec pr inherited a =
 	hov 0 (str "(" ++
                prlist_with_sep sep_v pr_name nal ++
                str ")" ++
-	       pr_simple_return_type pr na po ++ str " :=" ++
-               spc() ++ pr ltop c ++ str " in") ++
-        spc() ++ pr ltop b),
+	       pr_simple_return_type (pr mt) na po ++ str " :=" ++
+               pr spc ltop c ++ str " in") ++
+        pr spc ltop b),
       lletin
   | CIf (_,c,(na,po),b1,b2) ->
       (* On force les parenthèses autour d'un "if" sous-terme (même si le
 	 parsing est lui plus tolérant) *)
       hv 0 (
-	hov 1 (str "if " ++ pr ltop c ++ pr_simple_return_type pr na po) ++
+	hov 1 (str "if " ++ pr mt ltop c ++ pr_simple_return_type (pr mt) na po) ++
 	spc () ++
-	hov 0 (str "then" ++ brk (1,1) ++ pr ltop b1) ++ spc () ++
-	hov 0 (str "else" ++ brk (1,1) ++ pr ltop b2)),
+	hov 0 (str "then" ++ pr (fun () -> brk (1,1)) ltop b1) ++ spc () ++
+	hov 0 (str "else" ++ pr (fun () -> brk (1,1)) ltop b2)),
       lif
      
   | COrderedCase (_,st,po,c,[b1;b2]) when st = IfStyle ->
       (* On force les parenthèses autour d'un "if" sous-terme (même si le
 	 parsing est lui plus tolérant) *)
       hv 0 (
-	hov 1 (str "if " ++ pr ltop c ++ pr_return_type pr po) ++ spc () ++
-	hov 0 (str "then" ++ brk (1,1) ++ pr ltop b1) ++ spc () ++
-	hov 0 (str "else" ++ brk (1,1) ++ pr ltop b2)),
+	hov 1 (str "if " ++ pr mt ltop c ++
+                 pr_return_type (pr mt) po) ++ spc () ++
+	hov 0 (str "then" ++ pr (fun () -> brk (1,1)) ltop b1) ++ spc () ++
+	hov 0 (str "else" ++ pr (fun () -> brk (1,1)) ltop b2)),
       lif
   | COrderedCase (_,st,po,c,[CLambdaN(_,[nal,_],b)]) when st = LetStyle ->
       hv 0 (
@@ -502,18 +546,18 @@ let rec pr inherited a =
 	hov 0 (str "(" ++
                prlist_with_sep sep_v (fun (_,n) -> pr_name n) nal ++
                str ")" ++
-	       pr_return_type pr po ++ str " :=" ++
-               spc() ++ pr ltop c ++ str " in") ++
-        spc() ++ pr ltop b),
+	       pr_return_type (pr mt) po ++ str " :=" ++
+               pr spc ltop c ++ str " in") ++
+        pr spc ltop b),
       lletin
   | COrderedCase (_,style,po,c,bl) ->
       hv 0 (
 	str (if style=MatchStyle then "old_match " else "match ") ++ 
-	pr ltop c ++
-	pr_return_type pr po ++
+	pr mt ltop c ++
+	pr_return_type (pr mt) po ++
 	str " with" ++ brk (1,0) ++
 	hov 0 (prlist
-          (fun b -> str "| ??? =>" ++ spc() ++ pr ltop b ++ fnl ()) bl) ++
+          (fun b -> str "| ??? =>" ++ pr spc ltop b ++ fnl ()) bl) ++
         str "end"),
       latom
   | CHole _ -> str "_", latom
@@ -521,18 +565,21 @@ let rec pr inherited a =
   | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom
   | CSort (_,s) -> pr_sort s, latom
   | CCast (_,a,b) ->
-      hv 0 (pr (lcast,L) a ++ cut () ++ str ":" ++ pr (-lcast,E) b), lcast
+      hv 0 (pr mt (lcast,L) a ++ cut () ++ str ":" ++ pr mt (-lcast,E) b),
+      lcast
   | CNotation (_,"( _ )",[t]) ->
-      str"("++ pr (max_int,L) t ++ str")", latom
-  | CNotation (_,s,env) -> pr_notation pr s env
+      pr (fun()->str"(") (max_int,L) t ++ str")", latom
+  | CNotation (_,s,env) -> pr_notation (pr mt) s env
   | CNumeral (_,(Bignat.POS _ as p)) -> Bignat.pr_bigint p, lposint
   | CNumeral (_,(Bignat.NEG _ as p)) -> Bignat.pr_bigint p, lnegint
-  | CDelimiters (_,sc,a) -> pr_delimiters sc (pr lsimple a), 1
+  | CDelimiters (_,sc,a) -> pr_delimiters sc (pr mt lsimple a), 1
   | CDynamic _ -> str "<dynamic>", latom
   in
   let loc = constr_loc a in
   pr_with_comments loc
-    (if prec_less prec inherited then strm else surround strm)
+    (sep() ++ if prec_less prec inherited then strm else surround strm)
+
+let pr = pr mt
 
 let rec strip_context n iscast t =
   if n = 0 then
diff --git a/translate/ppconstrnew.mli b/translate/ppconstrnew.mli
index 968464f651..51c6f8b7f0 100644
--- a/translate/ppconstrnew.mli
+++ b/translate/ppconstrnew.mli
@@ -40,7 +40,15 @@ val pr_global : Idset.t -> global_reference -> std_ppcmds
 val pr_tight_coma : unit -> std_ppcmds
 val pr_located :
   ('a -> std_ppcmds) -> 'a located -> std_ppcmds
+val pr_lident : identifier located -> std_ppcmds
+val pr_lname : name located -> std_ppcmds
+
 val pr_with_comments : loc -> std_ppcmds -> std_ppcmds
+val pr_com_at : int -> std_ppcmds
+val pr_sep_com :
+  (unit -> std_ppcmds) ->
+  (constr_expr -> std_ppcmds) ->
+  constr_expr -> std_ppcmds
 val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
 val pr_name : name -> std_ppcmds
 val pr_qualid : qualid -> std_ppcmds
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index 9ff326b522..2373f73710 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -40,10 +40,6 @@ let strip_prod_binders_expr n ty =
       | _ -> error "Cannot translate fix tactic: not enough products" in
   strip_ty [] n ty
 
-let is_ident_expr = function
-    Topconstr.CRef(Ident _) -> true
-  | _ -> false
-
 
 (* In v8 syntax only double quote char is escaped by repeating it *)
 let rec escape_string_v8 s =
@@ -290,7 +286,7 @@ let pr_match_pattern pr_pat = function
       str "context " ++ pr_id id ++ str "[" ++ pr_pat a ++ str "]"
 
 let pr_match_hyps pr_pat = function
-  | Hyp (nal,mp) -> pr_located pr_name nal ++ str ":" ++ pr_match_pattern pr_pat mp
+  | Hyp (nal,mp) -> pr_lname nal ++ str ":" ++ pr_match_pattern pr_pat mp
 
 let pr_match_rule m pr pr_pat = function
   | Pat ([],mp,t) when m ->
@@ -308,10 +304,10 @@ let pr_funvar = function
 
 let pr_let_clause k pr = function
   | (id,None,t) ->
-      hov 0 (str k ++ pr_located pr_id id ++ str " :=" ++ brk (1,1) ++
+      hov 0 (str k ++ pr_lident id ++ str " :=" ++ brk (1,1) ++
              pr (TacArg t))
   | (id,Some c,t) ->
-      hv 0 (str k ++ pr_located pr_id id ++ str" :" ++ brk(1,2) ++
+      hv 0 (str k ++ pr_lident id ++ str" :" ++ brk(1,2) ++
       pr c ++
       str " :=" ++ brk (1,1) ++ pr (TacArg t))
 
@@ -324,7 +320,7 @@ let pr_let_clauses pr = function
 
 let pr_rec_clause pr (id,(l,t)) =
   hov 0
-    (pr_located pr_id id ++ prlist pr_funvar l ++ str " :=") ++ spc () ++ pr t
+    (pr_lident id ++ prlist pr_funvar l ++ str " :=") ++ spc () ++ pr t
 
 let pr_rec_clauses pr l = 
   prlist_with_sep (fun () -> fnl () ++ str "with ") (pr_rec_clause pr) l
@@ -374,7 +370,7 @@ let pr_then () = str ";"
 
 open Closure
 
-let make_pr_tac (pr_tac,pr_tac0,pr_constr,pr_lconstr,pr_pat,pr_cst,pr_ind,pr_ref,pr_ident,pr_extend,strip_prod_binders,is_ident) =
+let make_pr_tac (pr_tac,pr_tac0,pr_constr,pr_lconstr,pr_pat,pr_cst,pr_ind,pr_ref,pr_ident,pr_extend,strip_prod_binders) =
 
 let pr_bindings env = pr_bindings (pr_lconstr env) (pr_constr env) in
 let pr_ex_bindings env = pr_bindings_gen true (pr_lconstr env) (pr_constr env) in
@@ -387,10 +383,10 @@ let pr_intarg n = spc () ++ int n in
 
 let pr_binder_fix env (nal,t) =
 (*  match t with
-  | CHole _ -> spc() ++ prlist_with_sep spc (pr_located pr_name) nal
+  | CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal
   | _ ->*)
     let s =
-      prlist_with_sep spc (pr_located pr_name) nal ++ str ":" ++
+      prlist_with_sep spc (pr_lname) nal ++ str ":" ++
       pr_lconstr env t in
     spc() ++ hov 1 (str"(" ++ s ++ str")") in
 
@@ -469,7 +465,7 @@ and pr_atom1 env = function
   | TacIntroMove (ido1,Some id2) ->
       hov 1
       (str "intro" ++ pr_opt pr_id ido1 ++ spc () ++ str "after " ++
-       pr_located pr_id id2)
+       pr_lident id2)
   | TacAssumption as t -> pr_atom0 env t
   | TacExact c -> hov 1 (str "exact" ++ pr_constrarg env c)
   | TacApply cb -> hov 1 (str "apply" ++ spc () ++ pr_with_bindings env cb)
@@ -578,9 +574,9 @@ and pr_atom1 env = function
 (*  | TacAutoTDB None as x -> pr_atom0 env x
   | TacAutoTDB (Some n) -> hov 0 (str "autotdb" ++ spc () ++ int n)
   | TacDestructHyp (true,id) ->
-      hov 0 (str "cdhyp" ++ spc () ++ pr_located pr_id id)
+      hov 0 (str "cdhyp" ++ spc () ++ pr_lident id)
   | TacDestructHyp (false,id) ->
-      hov 0 (str "dhyp" ++ spc () ++ pr_located pr_id id)
+      hov 0 (str "dhyp" ++ spc () ++ pr_lident id)
   | TacDestructConcl as x -> pr_atom0 env x
   | TacSuperAuto (n,l,b1,b2) ->
       hov 1 (str "superauto" ++ pr_opt int n ++ pr_autoarg_adding l ++ 
@@ -749,8 +745,7 @@ let rec pr_tac env inherited tac =
       pr_with_comments loc (hov 1 (pr_atom1 env t)), ltatom
   | TacArg(Tacexp e) -> pr_tac0 env e, latom
   | TacArg(ConstrMayEval (ConstrTerm c)) ->
-      if is_ident c then pr_constr env c, latom
-      else str "constr:" ++ pr_constr env c, latom
+      str "constr:" ++ pr_constr env c, latom
   | TacArg(ConstrMayEval c) ->
       pr_may_eval (pr_constr env) (pr_lconstr env) (pr_cst env) c, leval
   | TacArg(TacFreshId sopt) -> str "fresh" ++ pr_opt qsnew sopt, latom
@@ -795,10 +790,6 @@ let strip_prod_binders_rawterm n (ty,_) =
         | _ -> error "Cannot translate fix tactic: not enough products" in
   strip_ty [] n ty
 
-let is_ident_rawterm = function
-    (Rawterm.RRef(_,VarRef _),_) -> true
-  | _ -> false
-
 let strip_prod_binders_constr n ty =
   let rec strip_ty acc n ty =
     if n=0 then (List.rev acc, ty) else
@@ -818,9 +809,9 @@ let rec raw_printers =
      (fun _ -> pr_reference),
      (fun _ -> pr_reference),
      pr_reference,
-     pr_or_metaid (pr_located pr_id),
+     pr_or_metaid pr_lident,
      Pptactic.pr_raw_extend,
-     strip_prod_binders_expr, is_ident_expr)
+     strip_prod_binders_expr)
 
 and pr_raw_tactic env (t:raw_tactic_expr) =
   pi1 (make_pr_tac raw_printers) env t
@@ -843,9 +834,9 @@ let rec glob_printers =
      (fun env -> pr_or_var (pr_and_short_name (pr_evaluable_reference_env env))),
      (fun vars -> pr_or_var (pr_inductive vars)),
      pr_ltac_or_var (pr_located pr_ltac_constant),
-     pr_located pr_id,
+     pr_lident,
      Pptactic.pr_glob_extend,
-     strip_prod_binders_rawterm, is_ident_rawterm)
+     strip_prod_binders_rawterm)
 
 and pr_glob_tactic env (t:glob_tactic_expr) =
   pi1 (make_pr_tac glob_printers) env t
@@ -868,5 +859,5 @@ let (pr_tactic,_,_) =
      pr_ltac_constant,
      pr_id,
      Pptactic.pr_extend,
-     strip_prod_binders_constr,Term.isVar)
+     strip_prod_binders_constr)
 
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 2612a59254..78d8f1bf71 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -28,9 +28,20 @@ open Topconstr
 open Decl_kinds
 open Tacinterp
 
+let pr_spc_type = pr_sep_com spc pr_type
+
 (* Copie de Nameops *)
 let pr_id id = pr_id (Constrextern.v7_to_v8_id id)
 
+let pr_lident (b,_ as loc,id) =
+  if loc <> dummy_loc then
+    pr_located pr_id ((b,b+String.length(string_of_id id)),id)
+  else pr_id id
+
+let pr_lname = function
+    (loc,Name id) -> pr_lident (loc,id)
+  | lna -> pr_located pr_name lna
+
 let pr_ltac_id id = pr_id (id_of_ltac_v7_id id)
 
 let pr_module r =
@@ -99,8 +110,6 @@ let sep_v = fun _ -> str","
 let sep_v2 = fun _ -> str"," ++ spc()
 let sep_pp = fun _ -> str":"
 
-let pr_located pr (loc,x) = pr x
-
 let pr_ne_sep sep pr = function
     [] -> mt()
   | l -> sep() ++ pr l
@@ -228,9 +237,9 @@ let pr_hints local db h pr_c pr_pat =
 let pr_with_declaration pr_c = function
   | CWith_Definition (id,c) ->
       let p = pr_c c in
-      str"Definition" ++ spc() ++ pr_id id ++ str" := " ++ p
+      str"Definition" ++ spc() ++ pr_lident id ++ str" := " ++ p
   | CWith_Module (id,qid) ->
-      str"Module" ++ spc() ++ pr_id id ++ str" := " ++
+      str"Module" ++ spc() ++ pr_lident id ++ str" := " ++
       pr_located pr_qualid qid
 
 let rec pr_module_type pr_c = function
@@ -248,12 +257,12 @@ let pr_module_vardecls pr_c (idl,mty) =
   let m = pr_module_type pr_c mty in
   (* Update the Nametab for interpreting the body of module/modtype *)
   let lib_dir = Lib.library_dp() in
-  List.iter (fun id ->
+  List.iter (fun (_,id) ->
     Declaremods.process_module_bindings [id]
       [make_mbid lib_dir (string_of_id id),
        Modintern.interp_modtype (Global.env()) mty]) idl;
   (* Builds the stream *)
-  spc() ++ str"(" ++ prlist_with_sep spc pr_id idl ++ str":" ++ m ++ str")"
+  spc() ++ str"(" ++ prlist_with_sep spc pr_lident idl ++ str":" ++ m ++ str")"
 
 let pr_module_binders l pr_c = 
   (* Effet de bord complexe pour garantir la declaration des noms des
@@ -320,11 +329,15 @@ let pr_and_type_binders_arg bl =
   pr_binders_arg bl
 
 let pr_onescheme (id,dep,ind,s) =
-  hov 0 (pr_id id ++ str" :=") ++ spc() ++
+  hov 0 (pr_lident id ++ str" :=") ++ spc() ++
   hov 0 ((if dep then str"Induction for" else str"Minimality for")
   ++ spc() ++ pr_reference ind) ++ spc() ++ 
   hov 0 (str"Sort" ++ spc() ++ pr_sort s)
 
+let begin_of_inductive = function
+    [] -> 0
+  | (_,(((b,_),_),_))::_ -> b
+
 let pr_class_rawexpr = function
   | FunClass -> str"Funclass"
   | SortClass -> str"Sortclass"
@@ -344,7 +357,7 @@ let pr_assumption_token many = function
       anomaly "Don't know how to translate a local conjecture"
 
 let pr_params pr_c (xl,(c,t)) =
-  hov 2 (prlist_with_sep sep pr_id xl ++ spc() ++
+  hov 2 (prlist_with_sep sep pr_lident xl ++ spc() ++
          (if c then str":>" else str":" ++
          spc() ++ pr_c t))
 
@@ -467,8 +480,8 @@ let rec pr_vernac = function
   | VernacSuspend -> str"Suspend"
   | VernacUnfocus -> str"Unfocus"
   | VernacGoal c -> str"Goal" ++ pr_lconstrarg c
-  | VernacAbort id -> str"Abort" ++ pr_opt (pr_located pr_id) id
-  | VernacResume id -> str"Resume" ++ pr_opt (pr_located pr_id) id
+  | VernacAbort id -> str"Abort" ++ pr_opt pr_lident id
+  | VernacResume id -> str"Resume" ++ pr_opt pr_lident id
   | VernacUndo i -> if i=1 then str"Undo" else str"Undo" ++ pr_intarg i
   | VernacFocus i -> str"Focus" ++ pr_opt int i
   | VernacGo g -> 
@@ -496,7 +509,7 @@ let rec pr_vernac = function
   | VernacDebug b -> pr_topcmd b
 
   (* Resetting *)
-  | VernacResetName id -> str"Reset" ++ spc() ++ pr_located pr_id id
+  | VernacResetName id -> str"Reset" ++ spc() ++ pr_lident id
   | VernacResetInitial -> str"Reset Initial"
   | VernacBack i -> if i=1 then str"Back" else str"Back" ++ pr_intarg i
 
@@ -512,7 +525,7 @@ let rec pr_vernac = function
   | VernacLoad (f,s) -> str"Load" ++ if f then (spc() ++ str"Verbose"
   ++ spc()) else spc()  ++ qsnew s
   | VernacTime v -> str"Time" ++ spc() ++ pr_vernac v
-  | VernacVar id -> pr_id id
+  | VernacVar id -> pr_lident id
   
   (* Syntax *) 
   | VernacGrammar _ -> 
@@ -607,9 +620,10 @@ let rec pr_vernac = function
               | Some ty ->
                   let bl2,body,ty' = extract_def_binders c ty in
                   (bl2,CCast (dummy_loc,body,ty'),
-                   spc() ++ str":" ++ spc () ++
-                   pr_type_env_n (Global.env())
-                     (local_binders_length bl + local_binders_length bl2)
+                   spc() ++ str":" ++
+                   pr_sep_com spc
+                     (pr_type_env_n (Global.env())
+                       (local_binders_length bl + local_binders_length bl2))
                      (prod_rawconstr ty bl)) in
 	    let n = local_binders_length bl + local_binders_length bl2 in
 	    let iscast = d <> None in
@@ -618,26 +632,26 @@ let rec pr_vernac = function
 		(abstract_rawconstr (abstract_rawconstr body bl2) bl) in
             (pr_binders_arg bindings,ty,Some (pr_reduce red ++ ppred))
         | ProveBody (bl,t) ->
-            (pr_and_type_binders_arg bl, str" :" ++ spc () ++ pr_type t, None)
+            (pr_and_type_binders_arg bl, str" :" ++ pr_spc_type t, None)
       in
       let (binds,typ,c) = pr_def_body b in
-      hov 2 (pr_def_token d ++ spc() ++ pr_id id ++ binds ++ typ ++
+      hov 2 (pr_def_token d ++ spc() ++ pr_lident id ++ binds ++ typ ++
       (match c with
         | None -> mt()
         | Some cc -> str" :=" ++ spc() ++ cc))
 
   | VernacStartTheoremProof (ki,id,(bl,c),b,d) ->
-      hov 1 (pr_thm_token ki ++ spc() ++ pr_id id ++ spc() ++
+      hov 1 (pr_thm_token ki ++ spc() ++ pr_lident id ++ spc() ++
       (match bl with
         | [] -> mt()
         | _ -> error "Statements with local binders no longer supported")
-      ++ str":" ++ spc() ++ pr_type (rename_bound_variables id c))
+      ++ str":" ++ pr_spc_type (rename_bound_variables (snd id) c))
   | VernacEndProof Admitted -> str"Admitted"
   | VernacEndProof (Proved (opac,o)) -> (match o with
     | None -> if opac then str"Qed" else str"Defined"
     | Some (id,th) -> (match th with
-      |	None -> (if opac then str"Save" else str"Defined") ++ spc() ++ pr_id id
-      |	Some tok -> str"Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_id id)) 
+      |	None -> (if opac then str"Save" else str"Defined") ++ spc() ++ pr_lident id
+      |	Some tok -> str"Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_lident id)) 
   | VernacExactProof c ->
       hov 2 (str"Proof" ++ pr_lconstrarg c)
   | VernacAssumption (stre,l) ->
@@ -668,7 +682,7 @@ let rec pr_vernac = function
 
       let (ind_env,ind_impls,arityl) =
         List.fold_left
-          (fun (env, ind_impls, arl) (recname, _, _, arityc, _) ->
+          (fun (env, ind_impls, arl) ((_,recname), _, _, arityc, _) ->
             let arity = Constrintern.interp_type sigma env_params arityc in
 	    let fullarity = Termops.it_mkProd_or_LetIn arity params in
 	    let env' = Termops.push_rel_assum (Name recname,fullarity) env in
@@ -686,7 +700,7 @@ let rec pr_vernac = function
 
       let lparnames = List.map (fun (na,_,_) -> na) params in
       let impl = List.map
-	(fun (recname,_,_,arityc,_) ->
+	(fun ((_,recname),_,_,arityc,_) ->
 	  let arity = Constrintern.interp_type sigma env_params arityc in
 	  let fullarity =
             Termops.prod_it arity (List.map (fun (id,_,ty) -> (id,ty)) params)
@@ -707,18 +721,20 @@ let rec pr_vernac = function
       (* Fin calcul implicites *)
 
       let pr_constructor (coe,(id,c)) =
-        hov 2 (pr_id id ++ str" " ++
-               (if coe then str":>" else str":") ++ spc () ++
-               pr_type_env_n ind_env_params 0 c) in
+        hov 2 (pr_lident id ++ str" " ++
+               (if coe then str":>" else str":") ++
+                pr_sep_com spc (pr_type_env_n ind_env_params 0) c) in
       let pr_constructor_list l = match l with
         | [] -> mt()
         | _ ->
-            fnl() ++ str (if List.length l = 1 then "   " else " | ") ++
+            pr_com_at (begin_of_inductive l) ++
+            fnl() ++
+            str (if List.length l = 1 then "   " else " | ") ++
             prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l in
       let pr_oneind key (id,ntn,indpar,s,lc) =
 	hov 0 (
           str key ++ spc() ++
-          pr_id id ++ pr_and_type_binders_arg indpar ++ spc() ++ str":" ++ 
+          pr_lident id ++ pr_and_type_binders_arg indpar ++ spc() ++ str":" ++ 
 	  spc() ++ pr_type s ++ 
 	  str" :=") ++ pr_constructor_list lc ++ 
 	pr_decl_notation pr_constr ntn in
@@ -811,29 +827,29 @@ let rec pr_vernac = function
   | VernacRecord (b,(oc,name),ps,s,c,fs) ->
       let pr_record_field = function
         | (oc,AssumExpr (id,t)) ->
-            hov 1 (pr_id id ++
+            hov 1 (pr_lident id ++
             (if oc then str" :>" else str" :") ++ spc() ++
             pr_type t)
         | (oc,DefExpr(id,b,opt)) -> (match opt with
 	    | Some t ->
-                hov 1 (pr_id id ++
+                hov 1 (pr_lident id ++
                 (if oc then str" :>" else str" :") ++ spc() ++
                 pr_type t ++ str" :=" ++ pr_lconstr b)
 	    | None ->
-                hov 1 (pr_id id ++ str" :=" ++ spc() ++
+                hov 1 (pr_lident id ++ str" :=" ++ spc() ++
                 pr_lconstr b)) in
       hov 2
         (str (if b then "Record" else "Structure") ++
-         (if oc then str" > " else str" ") ++ pr_id name ++ 
+         (if oc then str" > " else str" ") ++ pr_lident name ++ 
           pr_and_type_binders_arg ps ++ str" :" ++ spc() ++ pr_type s ++ 
 	  str" := " ++
          (match c with
            | None -> mt()
-           | Some sc -> pr_id sc) ++
+           | Some sc -> pr_lident sc) ++
 	spc() ++ str"{"  ++
         hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}"))
-  | VernacBeginSection id -> hov 2 (str"Section" ++ spc () ++ pr_id id)
-  | VernacEndSegment id -> hov 2 (str"End" ++ spc() ++ pr_id id)
+  | VernacBeginSection id -> hov 2 (str"Section" ++ spc () ++ pr_lident id)
+  | VernacEndSegment id -> hov 2 (str"End" ++ spc() ++ pr_lident id)
   | VernacRequire (exp,spe,l) -> hov 2
       (str "Require" ++ pr_require_token exp ++ spc() ++
       (match spe with
@@ -855,24 +871,24 @@ let rec pr_vernac = function
   | VernacIdentityCoercion (s,id,c1,c2) ->
       hov 1 (
 	str"Identity Coercion" ++ (match s with | Local -> spc() ++
-	  str"Local" ++ spc() | Global -> spc()) ++ pr_id id ++ 
+	  str"Local" ++ spc() | Global -> spc()) ++ pr_lident id ++ 
 	spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++
 	spc() ++ pr_class_rawexpr c2)
 
   (* Modules and Module Types *)
   | VernacDefineModule (m,bl,ty,bd) ->
       let b = pr_module_binders_list bl pr_lconstr in 
-      hov 2 (str"Module " ++ pr_id m ++ b ++
+      hov 2 (str"Module " ++ pr_lident m ++ b ++
              pr_opt (pr_of_module_type pr_lconstr) ty ++
              pr_opt (fun me -> str ":= " ++ pr_module_expr me) bd)
   | VernacDeclareModule (id,bl,m1,m2) ->
       let b = pr_module_binders_list bl pr_lconstr in 
-      hov 2 (str"Declare Module " ++ pr_id id ++ b ++
+      hov 2 (str"Declare Module " ++ pr_lident id ++ b ++
              pr_opt (pr_of_module_type pr_lconstr) m1 ++
              pr_opt (fun me -> str ":= " ++ pr_module_expr me) m2)
   | VernacDeclareModuleType (id,bl,m) ->
       let b = pr_module_binders_list bl pr_lconstr in 
-      hov 2 (str"Module Type " ++ pr_id id ++ b ++
+      hov 2 (str"Module Type " ++ pr_lident id ++ b ++
              pr_opt (fun mt -> str ":= " ++ pr_module_type pr_lconstr mt) m)
 
   (* Solving *)
@@ -919,7 +935,8 @@ let rec pr_vernac = function
 	    | Tacexpr.TacFun (idl,b) -> idl,b
             | _ -> [], body in
         pr_located pr_ltac_id id ++ 
-	prlist (function None -> str " _" | Some id -> spc () ++ pr_id id) idl
+	prlist (function None -> str " _"
+                       | Some id -> spc () ++ pr_id id) idl
 	++ str" :=" ++ brk(1,1) ++
 	let idl = List.map out_some (List.filter (fun x -> not (x=None)) idl)in
         pr_raw_tactic_env 
@@ -935,10 +952,10 @@ let rec pr_vernac = function
   | VernacHints (local,dbnames,h) ->
       pr_hints local dbnames h pr_constr pr_pattern
   | VernacSyntacticDefinition (id,c,None) ->
-      hov 2 (str"Syntactic Definition " ++ pr_id id ++ str" :=" ++
+      hov 2 (str"Syntactic Definition " ++ pr_lident id ++ str" :=" ++
              pr_lconstrarg c)
   | VernacSyntacticDefinition (id,c,Some n) ->
-      hov 2 (str"Syntactic Definition " ++ pr_id id ++ str" :=" ++
+      hov 2 (str"Syntactic Definition " ++ pr_lident id ++ str" :=" ++
              pr_lconstrarg c ++ spc() ++ str"|" ++ int n)
   | VernacDeclareImplicits (q,None) ->
       hov 2 (str"Implicit Arguments" ++ spc() ++ pr_reference q)
@@ -951,7 +968,7 @@ let rec pr_vernac = function
   | VernacReserve (idl,c) ->
       hov 1 (str"Implicit Type" ++
         str (if List.length idl > 1 then "s " else " ") ++
-        prlist_with_sep spc pr_id idl ++ str " :" ++ spc () ++ pr_type c)
+        prlist_with_sep spc pr_lident idl ++ str " :" ++ spc () ++ pr_type c)
   | VernacSetOpacity (fl,l) ->
       hov 1 ((if fl then str"Opaque" else str"Transparent") ++
              spc() ++ prlist_with_sep sep pr_reference l)