From 094b577f61f105f0a92f3f84d7e739884dd993a7 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 19 Nov 2017 05:11:18 +0100
Subject: [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`.
---
 vernac/command.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/command.ml b/vernac/command.ml
index be54f97b72..0232d7376c 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
-- 
cgit v1.2.3