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 /interp/constrintern.ml | |
| 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 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c4e0ac500..ee3e11f8a 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -24,7 +24,6 @@ open Constrexpr open Constrexpr_ops open Notation_term open Notation_ops -open Topconstr open Nametab open Notation open Inductiveops |