diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-21 09:19:58 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-21 09:19:58 +0000 |
| commit | fe8751f3d9372e88ad861b55775f912e92ae7016 (patch) | |
| tree | f11435f591d838f2751bd6a78468cbbe3b897884 /proofs/clenvtac.ml | |
| parent | c4ed1e18335c74750a55b22fc1d9c824fa32dc11 (diff) | |
In "progress", extending the set of evars w/o solving an existing one is
no longer considered a progress (this prepares generally having tactics
with arguments that contains holes that are added to the goal sigma).
Incidentally, made that "clear" now restricts evars only if the
restriction is really needed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12602 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/clenvtac.ml')
0 files changed, 0 insertions, 0 deletions