aboutsummaryrefslogtreecommitdiff
path: root/dev/base_include
diff options
context:
space:
mode:
authorherbelin2011-09-25 18:07:06 +0000
committerherbelin2011-09-25 18:07:06 +0000
commita638cba857c9a93a62f35bcceab6fa2c710805d2 (patch)
treed6ca6ede23703333e34058b8113f5ef521583891 /dev/base_include
parent85dae158c3225dc0dde6762e50f6fdef2203fdd5 (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 'dev/base_include')
0 files changed, 0 insertions, 0 deletions