From 744e7f6a319f4d459a3cc2309f575d43041d75aa Mon Sep 17 00:00:00 2001
From: barras
Date: Mon, 16 Oct 2006 17:11:44 +0000
Subject: affichage des ... dans les scripts

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9244 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/interface/showproof.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'contrib/interface')

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";
-- 
cgit v1.2.3