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`.
---
 API/API.mli | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'API/API.mli')

diff --git a/API/API.mli b/API/API.mli
index 704f1a3569..44d02ce2b9 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4389,6 +4389,8 @@ sig
   val default_binder_kind : Constrexpr.binder_kind
   val mkLetInC : Names.Name.t Loc.located * Constrexpr.constr_expr * Constrexpr.constr_expr option * Constrexpr.constr_expr -> Constrexpr.constr_expr
   val mkCProdN : ?loc:Loc.t -> Constrexpr.local_binder_expr list -> Constrexpr.constr_expr -> Constrexpr.constr_expr
+  val replace_vars_constr_expr :
+    Names.Id.t Names.Id.Map.t -> Constrexpr.constr_expr -> Constrexpr.constr_expr
 end
 
 module Notation_ops :
@@ -4443,8 +4445,11 @@ end
 
 module Topconstr :
 sig
+
   val replace_vars_constr_expr :
-  Names.Id.t Names.Id.Map.t -> Constrexpr.constr_expr -> Constrexpr.constr_expr
+    Names.Id.t Names.Id.Map.t -> Constrexpr.constr_expr -> Constrexpr.constr_expr
+  [@@ocaml.deprecated "use Constrexpr_ops.free_vars_of_constr_expr"]
+
 end
 
 module Constrintern :
-- 
cgit v1.2.3