diff options
author | 2017-12-12 19:36:15 +0100 | |
---|---|---|
committer | 2017-12-27 11:52:57 +0100 | |
commit | 05fc0542f6c7a15b9187a2a91beb0aa7a42bb2fa (patch) | |
tree | 97eccce3247c2d6d79d9b3cde4bc86410bd1d02c /plugins/ltac/profile_ltac_tactics.ml4 | |
parent | 2a25e1a56460556f8b8dcef2a70cd0d2b9422383 (diff) |
Remove the local polymorphic flag hack.
Some code in typeclasses was even breaking the invariant that
use_polymorphic_flag should not be called twice, but that code was
morally dead it seems, so we remove it.
Diffstat (limited to 'plugins/ltac/profile_ltac_tactics.ml4')
0 files changed, 0 insertions, 0 deletions