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`.
---
 parsing/egramcoq.ml  | 2 +-
 parsing/g_vernac.ml4 | 6 ------
 2 files changed, 1 insertion(+), 7 deletions(-)

(limited to 'parsing')

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index d51b8b54e5..7f50fd22ac 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, [])
 
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index a5b58b8553..82306bb9f5 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -129,12 +129,6 @@ let test_plural_form_types loc kwd = function
      warn_plural_command ~loc:!@loc kwd
   | _ -> ()
 
-let fresh_var env c =
-  Namegen.next_ident_away (Id.of_string "pat")
-    (List.fold_left (fun accu id -> Id.Set.add id accu) (Topconstr.free_vars_of_constr_expr c) env)
-
-let _ = Hook.set Constrexpr_ops.fresh_var_hook fresh_var
-
 (* Gallina declarations *)
 GEXTEND Gram
   GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion
-- 
cgit v1.2.3