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`.
---
 interp/interp.mllib | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'interp/interp.mllib')

diff --git a/interp/interp.mllib b/interp/interp.mllib
index e3500cfeac..bb22cf468d 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -1,13 +1,13 @@
 Tactypes
 Stdarg
 Genintern
-Constrexpr_ops
 Notation_ops
-Ppextend
 Notation
-Dumpglob
 Syntax_def
 Smartlocate
+Constrexpr_ops
+Ppextend
+Dumpglob
 Topconstr
 Reserve
 Impargs
-- 
cgit v1.2.3