diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-09-25 18:07:06 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-09-25 18:07:06 +0000 |
| commit | a638cba857c9a93a62f35bcceab6fa2c710805d2 (patch) | |
| tree | d6ca6ede23703333e34058b8113f5ef521583891 /tactics/extratactics.ml4 | |
| parent | 85dae158c3225dc0dde6762e50f6fdef2203fdd5 (diff) | |
Polishing commits r14492, r14448 and r14407 (tactics propagate
conversion hints to kernel). Whether REVERTcast must be known from
coqchk is unclear. In the meantime, warn about the unstability of the
situation (see also bug #2599).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14495 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/extratactics.ml4')
0 files changed, 0 insertions, 0 deletions