traducteur: affiche les commentaires a l'interieur des commandes

extraction: pb avec les variables de section definies


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

5 files changed, 132 insertions, 66 deletions

diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 784c977dd8..5e5a3236b4 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -74,6 +74,8 @@ let pr_notation pr s env =
 let pr_delimiters key strm =
   strm ++ str ("%"^key)
 
+let surround p = str"(" ++ p ++ str")"
+
 open Rawterm
 
 let pr_opt pr = function
@@ -106,7 +108,15 @@ let pr_name = function
   | Anonymous -> str"_"
   | Name id -> pr_id (Constrextern.v7_to_v8_id id)
 
-let pr_located pr (loc,x) = pr x
+let pr_located pr ((b,e),x) =
+  if Options.do_translate() then comment b ++ pr x ++ comment e
+  else pr x
+
+let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp)
+
+let pr_or_var pr = function
+  | Genarg.ArgArg x -> pr x
+  | Genarg.ArgVar (loc,s) -> pr_with_comments loc (pr_id s)
 
 let las = 12
 
@@ -124,16 +134,15 @@ let rec pr_patt inh p =
   | CPatDelimiters (_,k,p) ->
       pr_delimiters k (pr_patt (latom,E) p), latom
   in
-  if prec_less prec inh then strm
-  else str"(" ++ strm ++ str")"
+  let loc = cases_pattern_loc p in
+  pr_with_comments loc (if prec_less prec inh then strm else surround strm)
 
-let pr_eqn pr (_,pl,rhs) =
+let pr_eqn pr (loc,pl,rhs) =
   spc() ++ hov 4
-    (str "| " ++
-     hov 0 (prlist_with_sep sep_v (pr_patt ltop) pl ++ str " =>") ++
-     spc() ++ pr ltop rhs)
-
-let surround p = str"(" ++ p ++ str")"
+    (pr_with_comments loc
+      (str "| " ++
+      hov 0 (prlist_with_sep sep_v (pr_patt ltop) pl ++ str " =>") ++
+      spc() ++ pr ltop rhs))
 
 let pr_binder many pr (nal,t) =
   match t with
@@ -371,13 +380,39 @@ let pr_app pr a l =
     pr (lapp,L) a  ++ 
     prlist (fun a -> spc () ++ pr_expl_args pr a) l)
 
+
+let cs = function
+  | CRef(Ident(_,i)) -> "ID"
+  | CRef(Qualid(_,q)) -> "Q"
+  | CFix(_,x,a) -> "FX"
+  | CCoFix(_,x,a) -> "CFX"
+  | CArrow(_,a,b) -> "->"
+  | CProdN(_,bl,a) -> "Pi"
+  | CLambdaN(_,bl,a) -> "L"
+  | CLetIn(_,x,a,b) -> "LET"
+  | CAppExpl(_,f,a) -> "@E"
+  | CApp(_,f,a) -> "@"
+  | CCases(_,p,a,br) -> "C"
+  | COrderedCase(_,s,p,a,br) -> "OC"
+  | CLetTuple(_,ids,p,a,b) -> "LC"
+  | CIf(_,e,p,a,b) -> "LI"
+  | CHole _ -> "?"
+  | CPatVar(_,v) -> "PV"
+  | CEvar(_,ev) -> "EV"
+  | CSort(_,s) -> "S"
+  | CCast(_,a,b) -> "::"
+  | CNotation(_,n,l) -> "NOT"
+  | CNumeral(_,i) -> "NUM"
+  | CDelimiters(_,s,e) -> "DEL"
+  | CDynamic(_,d) -> "DYN"
+
 let rec pr 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
       (if List.length fix = 1 & prec_less (fst inherited) ltop
-       then str"(" ++ p ++ str")" else p),
+       then surround p else p),
       lfix
   | CCoFix (_,id,cofix) ->
       hov 0 (str "cofix " ++ pr_recursive (pr_cofixdecl pr) (snd id) cofix),
@@ -494,8 +529,9 @@ let rec pr inherited a =
   | CDelimiters (_,sc,a) -> pr_delimiters sc (pr (latom,E) a), latom
   | CDynamic _ -> str "<dynamic>", latom
   in
-  if prec_less prec inherited then strm
-  else str"(" ++ strm ++ str")"
+  let loc = constr_loc a in
+  pr_with_comments loc
+    (if prec_less prec inherited then strm else surround strm)
 
 let rec strip_context n iscast t =
   if n = 0 then
diff --git a/translate/ppconstrnew.mli b/translate/ppconstrnew.mli
index 6952bed566..0cd5dcd3fa 100644
--- a/translate/ppconstrnew.mli
+++ b/translate/ppconstrnew.mli
@@ -38,9 +38,14 @@ val prec_less : int -> int * Ppextend.parenRelation -> bool
 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_with_comments : loc -> std_ppcmds -> std_ppcmds
 val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
 val pr_name : name -> std_ppcmds
 val pr_qualid : qualid -> std_ppcmds
+val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
+val pr_metaid : identifier -> std_ppcmds
 val pr_red_expr :
   ('a -> std_ppcmds) * ('a -> std_ppcmds) *  ('b -> std_ppcmds) ->
     ('a,'b) red_expr_gen -> std_ppcmds
@@ -59,7 +64,6 @@ val pr_cases_pattern : cases_pattern_expr -> std_ppcmds
 val pr_may_eval :
   ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> ('a,'b) may_eval
     -> std_ppcmds
-val pr_metaid : identifier -> std_ppcmds
 
 val pr_rawconstr_env : env -> rawconstr -> std_ppcmds
 val pr_lrawconstr_env : env -> rawconstr -> std_ppcmds
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index f82c227438..574b665019 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -23,6 +23,19 @@ open Genarg
 open Libnames
 open Pptactic
 
+(* In v8 syntax only double quote char is escaped by repeating it *)
+let rec escape_string_v8 s =
+  let rec escape_at s i =
+    if i<0 then s
+    else if s.[i] == '"' then
+      let s' = String.sub s 0 i^"\""^String.sub s i (String.length s - i) in
+      escape_at s' (i-1)
+    else escape_at s (i-1) in
+  escape_at s (String.length s - 1)
+
+let qstringnew s = str ("\""^escape_string_v8 s^"\"")
+let qsnew = qstringnew
+
 let translate_v7_ltac = function
   | "DiscrR" -> "discrR"
   | "Sup0" -> "prove_sup0"
@@ -106,7 +119,7 @@ let id_of_ltac_v7_id id =
 
 let pr_ltac_or_var pr = function
   | ArgArg x -> pr x
-  | ArgVar (_,id) -> pr_id (id_of_ltac_v7_id id)
+  | ArgVar (loc,id) -> pr_with_comments loc ( pr_id (id_of_ltac_v7_id id))
 
 let pr_id id = pr_id (Constrextern.v7_to_v8_id id)
 
@@ -191,7 +204,7 @@ let pr_clause_pattern pr_id = function
 
 let pr_induction_arg prc = function
   | ElimOnConstr c -> prc c
-  | ElimOnIdent (_,id) -> pr_id id
+  | ElimOnIdent (loc,id) -> pr_with_comments loc (pr_id id)
   | ElimOnAnonHyp n -> int n
 
 let pr_match_pattern pr_pat = function
@@ -200,7 +213,7 @@ let pr_match_pattern pr_pat = function
   | Subterm (Some id,a) -> pr_id id ++ str "[" ++ pr_pat a ++ str "]"
 
 let pr_match_hyps pr_pat = function
-  | Hyp ((_,na),mp) -> pr_name na ++ str ":" ++ pr_match_pattern pr_pat mp
+  | Hyp (nal,mp) -> pr_located pr_name nal ++ str ":" ++ pr_match_pattern pr_pat mp
 
 let pr_match_rule m pr pr_pat = function
   | Pat ([],mp,t) when m ->
@@ -217,11 +230,11 @@ let pr_funvar = function
   | Some id -> spc () ++ pr_id id
 
 let pr_let_clause k pr prc pr_cst = function
-  | ((_,id),None,t) ->
-      hov 0 (str k ++ pr_id id ++ str " :=" ++ brk (1,1) ++
+  | (id,None,t) ->
+      hov 0 (str k ++ pr_located pr_id id ++ str " :=" ++ brk (1,1) ++
              pr (TacArg t))
-  | ((_,id),Some c,t) ->
-      hv 0 (str k ++ pr_id id ++ str" :" ++ brk(1,2) ++
+  | (id,Some c,t) ->
+      hv 0 (str k ++ pr_located pr_id id ++ str" :" ++ brk(1,2) ++
       pr_may_eval prc prc pr_cst c ++
       str " :=" ++ brk (1,1) ++ pr (TacArg t))
 
@@ -232,8 +245,9 @@ let pr_let_clauses pr prc pr_cst = function
          prlist (fun t -> spc () ++ pr_let_clause "with " pr prc pr_cst t) tl)
   | [] -> anomaly "LetIn must declare at least one binding"
 
-let pr_rec_clause pr ((_,id),(l,t)) =
-  hov 0 (pr_id id ++ prlist pr_funvar l ++ str " :=") ++ spc () ++ pr t
+let pr_rec_clause pr (id,(l,t)) =
+  hov 0
+    (pr_located pr_id 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
@@ -295,10 +309,13 @@ let rec pr_atom0 env = function
 
   (* Main tactic printer *)
 and pr_atom1 env = function
-  | TacExtend (_,s,l) ->
-      pr_extend (pr_constr env) (pr_lconstr env) (pr_tac env) s l
-  | TacAlias (_,s,l,_) ->
-      pr_extend (pr_constr env) (pr_lconstr env) (pr_tac env) s (List.map snd l)
+  | TacExtend (loc,s,l) ->
+      pr_with_comments loc 
+        (pr_extend (pr_constr env) (pr_lconstr env) (pr_tac env) s l)
+  | TacAlias (loc,s,l,_) ->
+      pr_with_comments loc
+        (pr_extend (pr_constr env) (pr_lconstr env) (pr_tac env) s
+          (List.map snd l))
 
   (* Basic tactics *)
   | TacIntroPattern [] as t -> pr_atom0 env t
@@ -308,9 +325,10 @@ and pr_atom1 env = function
       hv 1 (str "intros until" ++ pr_arg pr_quantified_hypothesis h)
   | TacIntroMove (None,None) as t -> pr_atom0 env t
   | TacIntroMove (Some id1,None) -> str "intro " ++ pr_id id1
-  | TacIntroMove (ido1,Some (_,id2)) ->
+  | TacIntroMove (ido1,Some id2) ->
       hov 1
-      (str "intro" ++ pr_opt pr_id ido1 ++ spc () ++ str "after " ++ pr_id id2)
+      (str "intro" ++ pr_opt pr_id ido1 ++ spc () ++ str "after " ++
+       pr_located pr_id 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)
@@ -403,8 +421,10 @@ and pr_atom1 env = function
   | TacAuto (n,db) -> hov 0 (str "auto" ++ pr_opt int n ++ pr_hintbases db)
   | 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_id id)
-  | TacDestructHyp (false,(_,id)) -> hov 0 (str "dhyp" ++ spc () ++ pr_id id)
+  | TacDestructHyp (true,id) ->
+      hov 0 (str "cdhyp" ++ spc () ++ pr_located pr_id id)
+  | TacDestructHyp (false,id) ->
+      hov 0 (str "dhyp" ++ spc () ++ pr_located pr_id 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 ++ 
@@ -555,21 +575,23 @@ let rec pr_tac env inherited tac =
   | TacFail (0,"") -> str "fail", latom
   | TacFail (n,s) -> 
       str "fail" ++ (if n=0 then mt () else pr_arg int n) ++
-      (if s="" then mt() else str " \"" ++ str s ++ str "\""), latom
+      (if s="" then mt() else qsnew s), latom
   | TacFirst tl ->
       str "first" ++ spc () ++ pr_seq_body (pr_tac env) tl, llet
   | TacSolve tl ->
       str "solve" ++ spc () ++ pr_seq_body (pr_tac env) tl, llet
   | TacId -> str "idtac", latom
-  | TacAtom (_,t) -> hov 1 (pr_atom1 env t), ltatom
+  | TacAtom (loc,t) ->
+      pr_with_comments loc (hov 1 (pr_atom1 env t)), ltatom
   | TacArg(Tacexp e) -> pr_tac0 env e, latom
   | TacArg(ConstrMayEval (ConstrTerm c)) -> str "'" ++ pr_constr env c, latom
   | TacArg(ConstrMayEval c) ->
       pr_may_eval (pr_constr env) (pr_lconstr env) (pr_cst env) c, leval
   | TacArg(Integer n) -> int n, latom
-  | TacArg(TacCall(_,f,l)) ->
-      hov 1 (pr_ref f ++ spc () ++
-             prlist_with_sep spc (pr_tacarg env) l),
+  | TacArg(TacCall(loc,f,l)) ->
+      pr_with_comments loc
+        (hov 1 (pr_ref f ++ spc () ++
+         prlist_with_sep spc (pr_tacarg env) l)),
       lcall
   | TacArg a -> pr_tacarg env a, latom
   in
@@ -577,13 +599,14 @@ let rec pr_tac env inherited tac =
   else str"(" ++ strm ++ str")"
 
 and pr_tacarg env = function
-  | TacDynamic (_,t) -> str ("<dynamic ["^(Dyn.tag t)^"]>")
-  | MetaIdArg (_,s) -> str ("$" ^ s)
+  | TacDynamic (loc,t) ->
+      pr_with_comments loc (str ("<dynamic ["^(Dyn.tag t)^"]>"))
+  | MetaIdArg (loc,s) -> pr_with_comments loc (str ("$" ^ s))
   | Identifier id -> pr_id id
   | TacVoid -> str "()"
   | Reference r -> pr_ref r
   | ConstrMayEval (ConstrTerm c) -> pr_constr env c
-  | TacFreshId sopt -> str "fresh" ++ pr_opt qstring sopt
+  | TacFreshId sopt -> str "fresh" ++ pr_opt qsnew sopt
   | (ConstrMayEval _|TacCall _|Tacexp _|Integer _) as a ->
       str "'" ++ pr_tac env (latom,E) (TacArg a)
 
diff --git a/translate/pptacticnew.mli b/translate/pptacticnew.mli
index 4e8e29a539..b6861f8160 100644
--- a/translate/pptacticnew.mli
+++ b/translate/pptacticnew.mli
@@ -15,6 +15,8 @@ open Proof_type
 open Topconstr
 open Names
 
+val qsnew : string -> std_ppcmds
+
 val pr_raw_tactic : Environ.env -> raw_tactic_expr -> std_ppcmds
  
 val pr_glob_tactic : Environ.env -> glob_tactic_expr -> std_ppcmds
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 0f3d54ed5e..81818bb08d 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -36,9 +36,11 @@ let pr_ltac_id id = pr_id (id_of_ltac_v7_id id)
 let pr_module = Libnames.pr_reference
 
 let pr_reference r =
+  let loc = loc_of_reference r in
   try match Nametab.extended_locate (snd (qualid_of_reference r)) with
     | TrueGlobal ref ->
-	pr_reference (Constrextern.extern_reference dummy_loc Idset.empty ref)
+        pr_with_comments loc
+	  (pr_reference (Constrextern.extern_reference loc Idset.empty ref))
     | SyntacticDef kn ->
 	let is_coq_root d =
 	  let d = repr_dirpath d in
@@ -55,19 +57,17 @@ let pr_reference r =
 		  (reference_of_constr (Coqlib.build_coq_eq_data ()).Coqlib.sym)
               | _ -> r)
           else r
-	in pr_reference r
+	in pr_with_comments loc (pr_reference r)
   with Not_found ->
     error_global_not_found (snd (qualid_of_reference r))
 
-let quote str = "\""^str^"\""
-
 let sep_end () = str"."
 
 let start_theorem = ref false
 
 let insert_proof_keyword () =
   if !start_theorem then 
-    (start_theorem := false; str "Proof" ++ sep_end () ++ fnl())
+    (start_theorem := false; hv 0 (str "Proof" ++ sep_end () ++ fnl()))
   else
     mt ()
 
@@ -153,7 +153,7 @@ let pr_production_item = function
 
 let pr_comment pr_c = function
   | CommentConstr c -> pr_c c
-  | CommentString s -> qs s
+  | CommentString s -> qsnew s
   | CommentInt n -> int n
 
 let pr_in_out_modules = function
@@ -176,7 +176,7 @@ let pr_class_rawexpr = function
 
 let pr_option_ref_value = function
   | QualidRefValue id -> pr_reference id
-  | StringRefValue s -> qs s
+  | StringRefValue s -> qsnew s
 
 let pr_printoption a b = match a with
   | Goptions.PrimaryTable table -> str table ++ pr_opt (prlist_with_sep sep pr_option_ref_value) b
@@ -310,7 +310,7 @@ let pr_type_option pr_c = function
 
 let pr_decl_notation =
   pr_opt (fun (ntn,scopt) -> 
-    str "as " ++ str (quote ntn) ++ 
+    str "as " ++ qsnew ntn ++
     pr_opt (fun sc -> str " :" ++ str sc) scopt)
 
 let rec abstract_rawconstr c = function
@@ -415,12 +415,12 @@ let pr_grammar_tactic_rule (name,(s,pil),t) =
 (*
   hov 0 (
   (* str name ++ spc() ++ *)
-  hov 0 (str"[" ++ qs s ++ spc() ++
+  hov 0 (str"[" ++ qsnew s ++ spc() ++
   prlist_with_sep sep pr_production_item pil ++ str"]") ++
   spc() ++ hov 0 (str"->" ++ spc() ++ str"[" ++ pr_raw_tactic t ++ str"]"))
 *)
   hov 2 (str "Tactic Notation" ++ spc() ++ 
-    hov 0 (qs s ++ spc() ++ prlist_with_sep sep pr_production_item pil ++
+    hov 0 (qsnew s ++ spc() ++ prlist_with_sep sep pr_production_item pil ++
     spc() ++ str":= " ++ spc() ++ pr_raw_tactic t))
 
 let pr_box b = let pr_boxkind = function
@@ -434,14 +434,14 @@ in str"<" ++ pr_boxkind b ++ str">"
 let pr_paren_reln_or_extern = function
   | None,L -> str"L"
   | None,E -> str"E"
-  | Some pprim,Any -> qs pprim
-  | Some pprim,Prec p -> qs pprim ++ spc() ++ str":" ++ spc() ++ int p
+  | Some pprim,Any -> qsnew pprim
+  | Some pprim,Prec p -> qsnew pprim ++ spc() ++ str":" ++ spc() ++ int p
   | _ -> mt()
 
 let rec pr_next_hunks = function 
   | UNP_FNL -> str"FNL"
   | UNP_TAB -> str"TAB"
-  | RO c -> qs c
+  | RO c -> qsnew c
   | UNP_BOX (b,ll) -> str"[" ++ pr_box b ++ prlist_with_sep sep pr_next_hunks ll ++ str"]"
   | UNP_BRK (n,m) -> str"[" ++ int n ++ spc() ++ int m ++ str"]"
   | UNP_TBRK (n,m) -> str"[ TBRK" ++ int n ++ spc() ++ int m ++ str"]"
@@ -511,12 +511,13 @@ let rec pr_vernac = function
   | VernacBack i -> if i=1 then str"Back" else str"Back" ++ pr_intarg i
 
   (* State management *)
-  | VernacWriteState s -> str"Write State" ++ spc () ++ qs s
-  | VernacRestoreState s -> str"Restore State" ++ spc() ++ qs s
+  | VernacWriteState s -> str"Write State" ++ spc () ++ qsnew s
+  | VernacRestoreState s -> str"Restore State" ++ spc() ++ qsnew s
 
   (* Control *)
   | VernacList l -> hov 2 (str"[" ++ spc() ++ prlist_with_sep (fun _ -> sep_end () ++ fnl() ) (pr_located pr_vernac) l ++ spc() ++ str"]") 
-  | VernacLoad (f,s) -> str"Load" ++ if f then (spc() ++ str"Verbose" ++ spc()) else spc()  ++ str "\"" ++ str s ++ str "\""
+  | 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
   
@@ -554,14 +555,14 @@ let rec pr_vernac = function
 	    (match a with None -> [] | Some a -> [SetAssoc a]),s
         | None -> [],s in
       hov 0 (hov 0 (str"Infix " ++ pr_locality local
-      ++ qs s ++ spc() ++ pr_reference q) ++
+      ++ qsnew s ++ spc() ++ pr_reference q) ++
       pr_syntax_modifiers mv8 ++
       (match sn with
     | None -> mt()
     | Some sc -> spc() ++ str":" ++ spc() ++ str sc))
   | VernacDistfix (local,a,p,s,q,sn) ->
       hov 0 (str"Distfix " ++ pr_locality local ++ pr_entry_prec a ++ int p
-        ++ spc() ++ qs s ++ spc() ++ pr_reference q ++ (match sn with
+        ++ spc() ++ qsnew s ++ spc() ++ pr_reference q ++ (match sn with
     | None -> mt()
     | Some sc -> spc() ++ str":" ++ spc() ++ str sc))
   | VernacNotation (local,c,sl,mv8,opt) ->
@@ -572,7 +573,7 @@ let rec pr_vernac = function
 	let n = String.length s in
 	if n > 2 & s.[0] = '\'' & s.[n-1] = '\'' 
 	then str (String.sub s 1 (n-2))
-	else qs s in
+	else qsnew s in
       hov 2( str"Notation" ++ spc() ++ pr_locality local ++ ps ++
       str " :=" ++ pr_constrarg c ++ pr_syntax_modifiers l ++
       (match opt with
@@ -582,7 +583,7 @@ let rec pr_vernac = function
       let (s,l) = match mv8 with
           None -> out_some sl
         | Some ml -> ml in
-      str"Reserved Notation" ++ spc() ++ pr_locality local ++ qs s ++
+      str"Reserved Notation" ++ spc() ++ pr_locality local ++ qsnew s ++
       pr_syntax_modifiers l
 
   (* Gallina *)
@@ -919,20 +920,20 @@ pr_vbinders bl ++ spc())
         | None -> mt()
         | Some false -> str"Implementation" ++ spc()
         | Some true -> str"Specification" ++ spc ()) ++
-      qs f)
+      qsnew f)
   | VernacAddLoadPath (fl,s,d) -> hov 2
       (str"Add" ++
        (if fl then str" Rec " else spc()) ++
-       str"LoadPath" ++ spc() ++ qs s ++
+       str"LoadPath" ++ spc() ++ qsnew s ++
        (match d with 
          | None -> mt()
          | Some dir -> spc() ++ str"as" ++ spc() ++ pr_dirpath dir)) 
-  | VernacRemoveLoadPath s -> str"Remove LoadPath" ++ qs s
+  | VernacRemoveLoadPath s -> str"Remove LoadPath" ++ qsnew s
   | VernacAddMLPath (fl,s) ->
-      str"Add" ++ (if fl then str" Rec " else spc()) ++ str"ML Path" ++ qs s
+      str"Add" ++ (if fl then str" Rec " else spc()) ++ str"ML Path" ++ qsnew s
   | VernacDeclareMLModule l ->
-      hov 2 (str"Declare ML Module" ++ spc() ++ prlist_with_sep sep qs l)
-  | VernacChdir s -> str"Cd" ++ pr_opt qs s
+      hov 2 (str"Declare ML Module" ++ spc() ++ prlist_with_sep sep qsnew l)
+  | VernacChdir s -> str"Cd" ++ pr_opt qsnew s
 
   (* Commands *)
   | VernacDeclareTacticDefinition (rc,l) ->
@@ -1051,9 +1052,9 @@ pr_vbinders bl ++ spc())
   | VernacLocate loc -> 
       let pr_locate =function
 	| LocateTerm qid ->  pr_reference qid
-	| LocateFile f -> str"File" ++ spc() ++ qs f
+	| LocateFile f -> str"File" ++ spc() ++ qsnew f
 	| LocateLibrary qid -> str"Library" ++ spc () ++ pr_module qid
-	| LocateNotation s -> str ("\""^s^"\"")
+	| LocateNotation s -> qsnew s
       in str"Locate" ++ spc() ++ pr_locate loc
   | VernacComments l ->
       hov 2