affichage des ... dans les scripts

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

1 files changed, 7 insertions, 2 deletions

diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml
index 484b30e985..4775763660 100644
--- a/parsing/tactic_printer.ml
+++ b/parsing/tactic_printer.ml
@@ -34,7 +34,7 @@ let pr_rule = function
   | Nested(cmpd,_) ->
       begin
 	match cmpd with 
-	    Tactic texp -> hov 0 (pr_tactic texp)
+	    Tactic (texp,_) -> hov 0 (pr_tactic texp)
 	  | Proof_instr (_,instr) -> hov 0 (pr_proof_instr instr)
       end
   | Daimon -> str "<Daimon>"
@@ -45,10 +45,15 @@ let pr_rule = function
          Change_evars *)
       str "Evar change"
 
+let uses_default_tac = function
+  | Nested(Tactic(_,dflt),_) -> dflt
+  | _ -> false
+
 (* Does not print change of evars *)
 let pr_rule_dot = function 
   | Change_evars -> mt ()
-  | r -> pr_rule r ++ str"."
+  | r ->
+      pr_rule r ++ if uses_default_tac r then str "..." else str"."
 
 exception Different