From a931a16236752b664b72b189fd5ff4f8f1a28012 Mon Sep 17 00:00:00 2001
From: glondu
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
---
 proofs/proof_type.ml  | 1 -
 proofs/proof_type.mli | 1 -
 2 files changed, 2 deletions(-)

(limited to 'proofs')

diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 72351d4d38..ff28ba8773 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -44,7 +44,6 @@ type prim_rule =
   | Change_evars
 
 type proof_tree = {
-  open_subgoals : int;
   goal : goal;
   ref : (rule * proof_tree list) option }
 
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 9a0f493afc..886c0db427 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -73,7 +73,6 @@ type prim_rule =
   if [ref = (Some(Nested(Tactic t,p),l))] then [p] is the proof
   that the goal can be proven if the goals in [l] are solved. *)
 type proof_tree = {
-  open_subgoals : int;
   goal : goal;
   ref : (rule * proof_tree list) option }
 
-- 
cgit v1.2.3