Diverses corrections de l'afficheur et du traducteur pour s'assurer de

la réversibilité de la traduction (correction enregistrement des
retours chariot dans le lexeur, correction affichage espace superflu
en tête des VERNAC EXTEND, correction affichage morphism_signature
dans extraargs.ml4, correction affichage clear dans pptactic.ml)


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

4 files changed, 14 insertions, 2 deletions

diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 2c17590a3f..0652958c31 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -383,6 +383,7 @@ let rec next_token = parser bp
       (("METAIDENT", get_buff len), (bp,ep))
   | [< ''.' as c; t = parse_after_dot bp c >] ep ->
       comment_stop bp;
+      if Options.do_translate() & t=("",".") then between_com := true;
       (t, (bp,ep))
   | [< ' ('a'..'z' | 'A'..'Z' | '_' as c);
        len = ident_tail (store 0 c) >] ep ->
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 0657765daf..76054c5996 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -617,6 +617,7 @@ let rec pr_atom0 env = function
   | TacTrivial ([],Some []) -> str "trivial"
   | TacAuto (None,[],Some []) -> str "auto"
   | TacReflexivity -> str "reflexivity"
+  | TacClear (true,[]) -> str "clear"
   | t -> str "(" ++ pr_atom1 env t ++ str ")"
 
   (* Main tactic printer *)
@@ -696,6 +697,7 @@ and pr_atom1 env = function
   | TacNewInduction (h,e,ids) ->
       hov 1 (str "induction" ++ spc () ++
 	     prlist_with_sep spc (pr_induction_arg (pr_constr env)) h ++
+	     pr_with_names ids ++
              pr_opt (pr_eliminator env) e)
   | TacSimpleDestruct h ->
       hov 1 (str "simple destruct" ++ pr_arg pr_quantified_hypothesis h)
@@ -736,6 +738,7 @@ and pr_atom1 env = function
       hov 1 (str "auto" ++ pr_opt (pr_or_var int) n ++ str "decomp" ++ pr_opt int p)
 
   (* Context management *)
+  | TacClear (true,[]) as t -> pr_atom0 env t
   | TacClear (keep,l) ->
       hov 1 (str "clear" ++ spc () ++ (if keep then str "- " else mt ()) ++
              prlist_with_sep spc pr_ident l)
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index f43f93bd90..c0aa771ae0 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -828,6 +828,13 @@ and pr_extend s cl =
   try
     let rls = List.assoc s (Egrammar.get_extend_vernac_grammars()) in
     let rl = match_vernac_rule (List.map Genarg.genarg_tag cl) rls in
+    let start,rl,cl =
+      match rl with
+	| Egrammar.TacTerm s :: rl -> str s, rl, cl
+	| Egrammar.TacNonTerm _ :: rl ->
+	    (* Will put an unnecessary extra space in front *)
+	    pr_gen (Global.env()) (List.hd cl), rl, List.tl cl 
+	| [] -> anomaly "Empty entry" in
     let (pp,_) =
       List.fold_left
         (fun (strm,args) pi ->
@@ -836,7 +843,7 @@ and pr_extend s cl =
                 (strm ++ pr_gen (Global.env()) (List.hd args),
                 List.tl args)
             | Egrammar.TacTerm s -> (strm ++ spc() ++ str s, args))
-        (mt(),cl) rl in
+        (start,cl) rl in
     hov 1 pp
   with Not_found ->
     hov 1 (str ("TODO("^s) ++ prlist_with_sep sep pr_arg cl ++ str ")")
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 6017115c46..665a7bd752 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -34,7 +34,8 @@ ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient
 END
 
 (* For Setoid rewrite *)
-let pr_morphism_signature _ _ _ = Setoid_replace.pr_morphism_signature
+let pr_morphism_signature _ _ _ s =
+  spc () ++ Setoid_replace.pr_morphism_signature s
 
 ARGUMENT EXTEND morphism_signature
  TYPED AS morphism_signature