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`. --- dev/base_include | 1 - 1 file changed, 1 deletion(-) (limited to 'dev/base_include') 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 -- cgit v1.2.3