diff options
| author | barras | 2006-10-16 17:11:44 +0000 |
|---|---|---|
| committer | barras | 2006-10-16 17:11:44 +0000 |
| commit | 744e7f6a319f4d459a3cc2309f575d43041d75aa (patch) | |
| tree | f130166bae5b1c1aa39860e8e5a2e79bfa284296 /contrib | |
| parent | 8fe195799d9bf4eb0c84fad3e9a79b78e6e224ec (diff) | |
affichage des ... dans les scripts
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9244 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/interface/showproof.ml | 8 | ||||
| -rw-r--r-- | contrib/xml/proofTree2Xml.ml4 | 2 |
2 files changed, 5 insertions, 5 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] *) |