aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/btauto
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-11-19 05:11:18 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-11-19 17:42:48 +0100
commit094b577f61f105f0a92f3f84d7e739884dd993a7 (patch)
tree33b39e64d139d2079734a84359707c2fa12451c3 /plugins/btauto
parentedf1a8f36f75861b822081b3825357e122b6937d (diff)
[parser] Remove unnecessary statically initialized hook.
Addded by c6d9d4fb142ef42634be25b60c0995b541e86629 ["Adding ability to put any pattern in binders, prefixed by a quote."] its current placement as well as the hook don't make a lot of sense. In particular, they prevent parts of Coq working without linking the parser. To this purpose, we need to consolidate the `Constrexpr` utilities. While we are at it we do so and remove the `Topconstr` module which is fully redundant with `Constrexpr_ops`.
Diffstat (limited to 'plugins/btauto')
0 files changed, 0 insertions, 0 deletions