aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-12-18 23:07:25 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-12-18 23:07:25 +0000
commitc0b215c309ea5f2c898bf8d7b8d07f93d74a20a4 (patch)
tree92128b4e34e280e891f75731d1b00f1e0f1ee7a0 /proofs
parent36da868408c3d73efa1b60c8185e5db25257534e (diff)
Documentation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1145 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
-rw-r--r--proofs/evar_refiner.mli12
-rw-r--r--proofs/proof_type.mli31
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 }