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 /parsing/egramcoq.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 'parsing/egramcoq.ml')
| -rw-r--r-- | parsing/egramcoq.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index d51b8b54e..7f50fd22a 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -440,7 +440,7 @@ let make_act : type r. r target -> _ -> r gen_eval = function CAst.make ~loc @@ CNotation (notation , env) | ForPattern -> fun notation loc env -> let invalid = List.exists (fun (_, b) -> not b) env.binders in - let () = if invalid then Topconstr.error_invalid_pattern_notation ~loc () in + let () = if invalid then Constrexpr_ops.error_invalid_pattern_notation ~loc () in let env = (env.constrs, env.constrlists) in CAst.make ~loc @@ CPatNotation (notation, env, []) |