MAJ commentaires

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2909 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 4 insertions, 6 deletions

diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index c9f8aca31..756370b80 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 b6a08ac8b..9c4bf5c47 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;