From a4347448697b26f77ea09d917144e2883c76d930 Mon Sep 17 00:00:00 2001
From: glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 6 Oct 2010 08:49:52 +0000
Subject: 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
---
 plugins/xml/proof2aproof.ml | 22 ----------------------
 1 file changed, 22 deletions(-)

(limited to 'plugins')

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
-- 
cgit v1.2.3