Documentation

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

2 files changed, 42 insertions, 1 deletions

diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 169fde57b..24ab10970 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -17,9 +17,21 @@ open Refiner
 val rc_of_pfsigma : proof_tree sigma -> readable_constraints
 val rc_of_glsigma : goal sigma -> readable_constraints
 
+(* a [walking_constraints] is a structure associated to a specific
+   goal; it collects all evars of which the goal depends.
+  It has the following structure:
+  [(identifying stamp, time stamp, 
+  { focus : set of evars among decls of which the goal depends;
+    hyps  : context of the goal;
+    decls : a superset of evars of which the goal may depend })]
+*)
 type walking_constraints
 
 type 'a result_w_tactic = walking_constraints -> walking_constraints * 'a
+
+(* A [w_tactic] is a tactic which modifies the a set of evars of which
+a goal depend, either by instantiating one, or by declaring a new
+dependent goal *)
 type w_tactic           = walking_constraints -> walking_constraints
 
 val local_Constraints : 
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index dbc4ba655..7025f450a 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -55,7 +55,36 @@ type enamed_declarations = ctxtty evar_map
    with some extra information for the program tactic *)
 type global_constraints  = enamed_declarations timestamped
 
-(* Signature useful to define the tactic type *)
+(* The type [goal sigma] is the type of subgoal. It has the following form
+\begin{verbatim}
+   it    = { evar_concl = [the conclusion of the subgoal]
+             evar_hyps = [the hypotheses of the subgoal]
+             evar_body = Evar_Empty;
+             evar_info = { pgm    : [The Realizer pgm if any]
+                           lc     : [Set of evar num occurring in subgoal] }}
+   sigma = { stamp = [an int characterizing the ed field, for quick compare]
+             ed : [A set of existential variables depending in the subgoal]
+               number of first evar,
+               it = { evar_concl = [the type of first evar]
+                      evar_hyps = [the context of the evar]
+                      evar_body = [the body of the Evar if any]
+                      evar_info = { pgm    : [Useless ??]
+                                    lc     : [Set of evars occurring
+                                              in the type of evar] } };
+               ...
+               number of last evar, 
+               it = { evar_concl = [the type of evar]
+                      evar_hyps = [the context of the evar]
+                      evar_body = [the body of the Evar if any]
+                      evar_info = { pgm    : [Useless ??]
+                                    lc     : [Set of evars occurring
+                                              in the type of evar] } } }
+   }
+\end{verbatim}
+*)
+
+(* The type constructor ['a sigma] adds an evar map to an object of
+  type ['a] (see below the form of a [goal sigma] *)
 type 'a sigma = { 
   it : 'a ; 
   sigma : global_constraints }