diff options
Diffstat (limited to 'proofs/proof_type.mli')
| -rw-r--r-- | proofs/proof_type.mli | 5 |
1 files changed, 2 insertions, 3 deletions
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; |