From 2c1fd9ac85aafb82fc9998c7d2fc72ffbb73e73d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 23 Jul 2002 15:00:32 +0000
Subject: MAJ commentaires

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2909 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/proof_type.ml  | 5 ++---
 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;
-- 
cgit v1.2.3