diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-06 08:49:52 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-06 08:49:52 +0000 |
| commit | a4347448697b26f77ea09d917144e2883c76d930 (patch) | |
| tree | d40d5fbbb7b7d63b683dbdf862348eb874823c04 /plugins/xml | |
| parent | a931a16236752b664b72b189fd5ff4f8f1a28012 (diff) | |
Remove unused unshare_proof_tree from xml plugin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13505 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |