diff options
Diffstat (limited to 'contrib/xml/proof2aproof.ml')
| -rw-r--r-- | contrib/xml/proof2aproof.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/xml/proof2aproof.ml b/contrib/xml/proof2aproof.ml index 5c5ac5d61..9220e8a4d 100644 --- a/contrib/xml/proof2aproof.ml +++ b/contrib/xml/proof2aproof.ml @@ -154,7 +154,7 @@ let extract_open_proof sigma pf = (*CSC: debugging stuff to be removed *) if ProofTreeHash.mem proof_tree_to_constr node then Pp.ppnl (Pp.(++) (Pp.str "#DUPLICATE INSERTION: ") - (Refiner.print_proof (Evd.evars_of !evd) [] node)) ; + (Tactic_printer.print_proof (Evd.evars_of !evd) [] node)) ; ProofTreeHash.add proof_tree_to_constr node unsharedconstr ; unshared_constrs := S.add unsharedconstr !unshared_constrs ; unsharedconstr |