diff options
| author | herbelin | 2000-12-18 23:07:25 +0000 |
|---|---|---|
| committer | herbelin | 2000-12-18 23:07:25 +0000 |
| commit | c0b215c309ea5f2c898bf8d7b8d07f93d74a20a4 (patch) | |
| tree | 92128b4e34e280e891f75731d1b00f1e0f1ee7a0 /proofs/evar_refiner.mli | |
| parent | 36da868408c3d73efa1b60c8185e5db25257534e (diff) | |
Documentation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1145 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/evar_refiner.mli')
| -rw-r--r-- | proofs/evar_refiner.mli | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index 169fde57bf..24ab109709 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 : |