aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.mli
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2015-02-12 18:54:10 +0100
committerPierre-Marie Pédrot2015-02-12 19:27:59 +0100
commite9b239881bc32dd15ac53b9463708030c95a9e0c (patch)
tree812a66f6d6343c89892703f0522467939779c31a /kernel/type_errors.mli
parentde8888e28ad793511ba2e2969516325b0be44330 (diff)
Focussing on message view in CoqIDE when a message is pushed.
Also fixes bug #4030.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions