aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/QArith
diff options
context:
space:
mode:
authorGravatar vsiles <vsiles@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-06-29 09:41:09 +0000
committerGravatar vsiles <vsiles@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-06-29 09:41:09 +0000
commit4dce356eacb7b9804c2e2398447dbbc3b0dc1383 (patch)
tree14f44a67e0d0ec5e835792ec238ac2a1ed7a59f5 /theories/QArith
parent7e2f953c3c19904616c43990fada92e762aadec9 (diff)
change the flag "internal" in declare/ind_tables from bool to
a 3 state type to allow: * KernelVerbose / KernelSilent : handle the display of messages launch by Coq * UserVerbose : handle the display of messages launch by user actions Coq will still behaves the same way (TODOs in the code mark the places where we can now change the behaviour). I'll remove them in a few days when we'll have agreed on the correct behaviour. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13217 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/QArith')
0 files changed, 0 insertions, 0 deletions