affichage des ... dans les scripts

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

8 files changed, 29 insertions, 26 deletions

diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index bec24af1be..997821c53a 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -157,15 +157,15 @@ let seq_to_lnhyp sign sign' cl =
 let rule_is_complex r =
    match r with
        Nested (Tactic 
-		 (TacArg (Tacexp _)
-		 |TacAtom (_,(TacAuto _|TacSymmetry _))),_) -> true
+		 ((TacArg (Tacexp _)
+		 |TacAtom (_,(TacAuto _|TacSymmetry _))),_),_) -> true
    |_ -> false
 ;;
 
 let rule_to_ntactic r =
    let rt =
      (match r with
-       Nested(Tactic t,_) -> t
+       Nested(Tactic (t,_),_) -> t
      | Prim (Refine h) -> TacAtom (dummy_loc,TacExact h)
      | _ -> TacAtom (dummy_loc, TacIntroPattern [])) in
    if rule_is_complex r
@@ -234,7 +234,7 @@ let  to_nproof sigma osign pf =
               (List.map (fun x -> (to_nproof_rec sigma sign x).t_proof)
 		 spfl) in
 	  (match r with
-	       Nested(Tactic (TacAtom (_, TacAuto _)),_) ->
+	       Nested(Tactic (TacAtom (_, TacAuto _),_),_) ->
 		 if spfl=[]
 		 then
 	      	   {t_info="to_prove";
diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4
index d382ef955c..dbdc79a802 100644
--- a/contrib/xml/proofTree2Xml.ml4
+++ b/contrib/xml/proofTree2Xml.ml4
@@ -141,7 +141,7 @@ Pp.ppnl (Pp.(++) (Pp.str
               (fun i n -> [< i ; (aux n old_hyps) >]) [<>] nodes)
 
      | {PT.goal=goal;
-        PT.ref=Some(PT.Nested (PT.Tactic tactic_expr,hidden_proof),nodes)} ->
+        PT.ref=Some(PT.Nested (PT.Tactic(tactic_expr,_),hidden_proof),nodes)} ->
          (* [hidden_proof] is the proof of the tactic;                     *)
          (* [nodes] are the proof of the subgoals generated by the tactic; *)
          (* [flat_proof] if the proof-tree obtained substituting [nodes]   *)
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
 
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 4037237026..5c9d2406ed 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -40,12 +40,6 @@ type prim_rule =
   | Move of bool * identifier * identifier
   | Rename of identifier * identifier
 
-(*s Proof trees. 
-  [ref] = [None] if the goal has still to be proved, 
-  and [Some (r,l)] if the rule [r] was applied to the goal
-  and gave [l] as subproofs to be completed. 
-  if [ref = (Some(Tactic (t,p),l))] then [p] is the proof 
-  that the goal can be proven if the goals in [l] are solved. *)
 type proof_tree = {
   open_subgoals : int;
   goal : goal;
@@ -59,7 +53,7 @@ and rule =
   | Change_evars
 
 and compound_rule=  
-  | Tactic of tactic_expr
+  | Tactic of tactic_expr * bool
   | Proof_instr of bool*proof_instr (* the boolean is for focus restrictions *)
 
 and goal = evar_info
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 74c36c9811..9c82239ef3 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -72,7 +72,7 @@ type prim_rule =
   [ref] = [None] if the goal has still to be proved, 
   and [Some (r,l)] if the rule [r] was applied to the goal
   and gave [l] as subproofs to be completed. 
-  if [ref = (Some(Tactic (t,p),l))] then [p] is the proof 
+  if [ref = (Some(Nested(Tactic t,p),l))] then [p] is the proof 
   that the goal can be proven if the goals in [l] are solved. *)
 type proof_tree = {
   open_subgoals : int;
@@ -87,7 +87,8 @@ and rule =
   | Change_evars
 
 and compound_rule= 
-  | Tactic of tactic_expr
+  (* the boolean of Tactic tells if the default tactic is used *)
+  | Tactic of tactic_expr * bool
   | Proof_instr of bool * proof_instr
 
 and goal = evar_info
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 3d65406b85..2c02fb6f1b 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -173,13 +173,14 @@ let abstract_operation syntax semantics gls =
        goal = gls.it;
        ref = Some(Nested(syntax,hidden_proof),spfl)})
 
-let abstract_tactic_expr te tacfun gls =
-  abstract_operation (Tactic te) tacfun gls	
+let abstract_tactic_expr ?(dflt=false) te tacfun gls =
+  abstract_operation (Tactic(te,dflt)) tacfun gls	
 
-let abstract_tactic te = abstract_tactic_expr (Tacexpr.TacAtom (dummy_loc,te))
+let abstract_tactic ?(dflt=false) te =
+  abstract_tactic_expr ~dflt (Tacexpr.TacAtom (dummy_loc,te))
 
-let abstract_extended_tactic s args = 
-  abstract_tactic (Tacexpr.TacExtend (dummy_loc, s, args))
+let abstract_extended_tactic ?(dflt=false) s args = 
+  abstract_tactic ~dflt (Tacexpr.TacExtend (dummy_loc, s, args))
 
 let refiner = function
   | Prim pr as r ->
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 0225e6443e..b4b37fdf39 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -35,11 +35,12 @@ type transformation_tactic = proof_tree -> (goal list * validation)
 (*s Hiding the implementation of tactics. *)
 
 (* [abstract_tactic tac] hides the (partial) proof produced by [tac] under
-   a single proof node *)
+   a single proof node. The boolean tells if the default tactic is used. *)
 val abstract_operation : compound_rule -> tactic -> tactic
-val abstract_tactic : atomic_tactic_expr -> tactic -> tactic
-val abstract_tactic_expr : tactic_expr -> tactic -> tactic
-val abstract_extended_tactic : string -> closed_generic_argument list -> tactic -> tactic
+val abstract_tactic : ?dflt:bool -> atomic_tactic_expr -> tactic -> tactic
+val abstract_tactic_expr : ?dflt:bool -> tactic_expr -> tactic -> tactic
+val abstract_extended_tactic :
+  ?dflt:bool -> string -> closed_generic_argument list -> tactic -> tactic
 
 val refiner : rule -> tactic
 val frontier : transformation_tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 2d98891167..d49163bfba 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2190,7 +2190,8 @@ let hide_interp t ot gl =
   let t = eval_tactic te in
   match ot with 
   | None -> abstract_tactic_expr (TacArg (Tacexp te)) t gl
-  | Some t' -> abstract_tactic_expr (TacArg (Tacexp te)) (tclTHEN t t') gl
+  | Some t' ->
+      abstract_tactic_expr ~dflt:true (TacArg (Tacexp te)) (tclTHEN t t') gl
 
 (***************************************************************************)
 (* Substitution at module closing time *)