aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.ml
diff options
context:
space:
mode:
authorHugo Herbelin2019-04-27 22:19:15 +0200
committerHugo Herbelin2019-04-27 22:19:15 +0200
commit9b2cbdcdaac203999484ef90225f6cba5e8052db (patch)
tree6fc2fb3cbbd8d3eb853fcf87c0218cca32bc6f37 /kernel/type_errors.ml
parentae4239d6a5f4afcd9b7321dba790ffd4a64994a1 (diff)
CoqiDE: Load coqide.keys after coqiderc (addressing part of #9899).
This avoids the modifiers keys to overwrite changes made in coqide.keys.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions