From a931a16236752b664b72b189fd5ff4f8f1a28012 Mon Sep 17 00:00:00 2001
From: glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 6 Oct 2010 08:49:50 +0000
Subject: Remove open_subgoals field of proof_tree

It looks obsolete, probably as a consequence of the new proof engine.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13504 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/xml/proof2aproof.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'plugins/xml')

diff --git a/plugins/xml/proof2aproof.ml b/plugins/xml/proof2aproof.ml
index 9d3288d83..35a90cd02 100644
--- a/plugins/xml/proof2aproof.ml
+++ b/plugins/xml/proof2aproof.ml
@@ -63,8 +63,7 @@ let nf_evar sigma ~preserve =
 (* Warning: statuses, goals, prim_rules and tactic_exprs are not unshared! *)
 let rec unshare_proof_tree =
  let module PT = Proof_type in
-  function {PT.open_subgoals = status ;
-	    PT.goal = goal ;
+  function {PT.goal = goal ;
 	    PT.ref = ref} ->
    let unshared_ref =
     match ref with
@@ -78,8 +77,7 @@ let rec unshare_proof_tree =
 	in
          Some (unshared_rule, List.map unshare_proof_tree pfs)
    in
-    {PT.open_subgoals = status ;
-     PT.goal = goal ;
+    {PT.goal = goal ;
      PT.ref = unshared_ref}
 ;;
 
-- 
cgit v1.2.3