aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/constr.ml
diff options
context:
space:
mode:
authorGravatar Arnaud Spiwack <arnaud@spiwack.net>2015-02-19 11:28:19 +0100
committerGravatar Arnaud Spiwack <arnaud@spiwack.net>2015-02-24 16:37:04 +0100
commit50edb9bb8d43b190996d1d85a2bfd95f52b2db19 (patch)
tree52eb6f73a5c6f9c00ade4a4937960740972603ad /kernel/constr.ml
parentebf4d8e58eeddaf5237447a9a0f21de48e72caa5 (diff)
[info_auto] & [info_trivial]: warning message to help users find [Info].
Diffstat (limited to 'kernel/constr.ml')
0 files changed, 0 insertions, 0 deletions