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, 4 insertions, 4 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";