aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/nsatz
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2016-07-07 15:49:29 +0200
committerGravatar Matthieu Sozeau <mattam@mattam.org>2016-07-07 15:49:29 +0200
commit8b890de3642bee1140b238348dd76138b3f1a3dc (patch)
tree450998b3004d28a7dd8c02353f2974301e08c93d /plugins/nsatz
parent294f9928e16fd541564dbe7f36b92e0fcf2c9eff (diff)
Do not use implicit type info for (x := t) bindings
This maintains compatibility, it is debatable if we should use implicit type information for lets to allow for coercions to fire. (Problem found in math-comp).
Diffstat (limited to 'plugins/nsatz')
0 files changed, 0 insertions, 0 deletions