diff options
| -rw-r--r-- | proofs/proof_type.ml | 5 | ||||
| -rw-r--r-- | proofs/proof_type.mli | 5 |
2 files changed, 4 insertions, 6 deletions
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index c9f8aca31b..756370b800 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -50,9 +50,8 @@ type 'a sigma = { [ref] = [None] if the goal has still to be proved, and [Some (r,l)] if the rule [r] was applied to the goal and gave [l] as subproofs to be completed. - [subproof] = [(Some p)] if [ref = (Some(Tactic t,l))]; - [p] is then the proof that the goal can be proven if the goals - in [l] are solved. *) + if [ref = (Some(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 = { status : pf_status; goal : goal; diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index b6a08ac8bf..9c4bf5c473 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -78,9 +78,8 @@ type 'a sigma = { [ref] = [None] if the goal has still to be proved, and [Some (r,l)] if the rule [r] was applied to the goal and gave [l] as subproofs to be completed. - [subproof] = [(Some p)] if [ref = (Some(Tactic t,l))]; - [p] is then the proof that the goal can be proven if the goals - in [l] are solved. *) + if [ref = (Some(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 = { status : pf_status; goal : goal; |