diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-19 05:11:18 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-19 17:42:48 +0100 |
| commit | 094b577f61f105f0a92f3f84d7e739884dd993a7 (patch) | |
| tree | 33b39e64d139d2079734a84359707c2fa12451c3 /vernac | |
| parent | edf1a8f36f75861b822081b3825357e122b6937d (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 'vernac')
| -rw-r--r-- | vernac/command.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/vernac/command.ml b/vernac/command.ml index be54f97b7..0232d7376 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -22,7 +22,6 @@ open Globnames open Nameops open Constrexpr open Constrexpr_ops -open Topconstr open Constrintern open Nametab open Impargs |