affichage des ... dans les scripts

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

4 files changed, 15 insertions, 18 deletions

diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 403723702..5c9d2406e 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 74c36c981..9c82239ef 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 3d65406b8..2c02fb6f1 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 0225e6443..b4b37fdf3 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