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 /dev/base_include | |
| 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 'dev/base_include')
| -rw-r--r-- | dev/base_include | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/dev/base_include b/dev/base_include index f2912e112..0c2bdb9a2 100644 --- a/dev/base_include +++ b/dev/base_include @@ -130,7 +130,6 @@ open Reserve open Syntax_def open Constrexpr open Constrexpr_ops -open Topconstr open Notation_term open Notation_ops open Prettyp |