diff options
Diffstat (limited to 'plugins/xml')
| -rw-r--r-- | plugins/xml/proof2aproof.ml | 22 |
1 files changed, 0 insertions, 22 deletions
diff --git a/plugins/xml/proof2aproof.ml b/plugins/xml/proof2aproof.ml index 35a90cd02..2d16190bc 100644 --- a/plugins/xml/proof2aproof.ml +++ b/plugins/xml/proof2aproof.ml @@ -59,28 +59,6 @@ let nf_evar sigma ~preserve = aux ;; -(* Unshares a proof-tree. *) -(* Warning: statuses, goals, prim_rules and tactic_exprs are not unshared! *) -let rec unshare_proof_tree = - let module PT = Proof_type in - function {PT.goal = goal ; - PT.ref = ref} -> - let unshared_ref = - match ref with - None -> None - | Some (rule,pfs) -> - let unshared_rule = - match rule with - PT.Nested (cmpd, pf) -> - PT.Nested (cmpd, unshare_proof_tree pf) - | other -> other - in - Some (unshared_rule, List.map unshare_proof_tree pfs) - in - {PT.goal = goal ; - PT.ref = unshared_ref} -;; - module ProofTreeHash = Hashtbl.Make (struct |