diff options
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 1 | ||||
| -rw-r--r-- | plugins/xml/proof2aproof.ml | 6 | ||||
| -rw-r--r-- | proofs/proof_type.ml | 1 | ||||
| -rw-r--r-- | proofs/proof_type.mli | 1 |
4 files changed, 2 insertions, 7 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 7a92c995c9..0236c30958 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -132,7 +132,6 @@ let daimon_tac gls = let daimon _ pftree = set_daimon_flag (); {pftree with - open_subgoals=0; ref=Some (Daimon,[])} let daimon_subtree = diff --git a/plugins/xml/proof2aproof.ml b/plugins/xml/proof2aproof.ml index 9d3288d83d..35a90cd02b 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} ;; 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 } |