diff options
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] *) |