[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`.

1 files changed, 35 insertions, 2 deletions

diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 7bd275e51..3ecb3d321 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -56,11 +56,11 @@ val mkCProdN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_exp
 
 (** @deprecated variant of mkCLambdaN *)
 val abstract_constr_expr : constr_expr -> local_binder_expr list -> constr_expr
+[@@ocaml.deprecated "deprecated variant of mkCLambdaN"]
 
 (** @deprecated variant of mkCProdN *)
 val prod_constr_expr : constr_expr -> local_binder_expr list -> constr_expr
-
-val fresh_var_hook : (Names.Id.t list -> Constrexpr.constr_expr -> Names.Id.t) Hook.t
+[@@ocaml.deprecated "deprecated variant of mkCProdN"]
 
 (** {6 Destructors}*)
 
@@ -83,3 +83,36 @@ val names_of_local_binders : local_binder_expr list -> Name.t located list
 val names_of_local_assums : local_binder_expr list -> Name.t located list
 (** Same as [names_of_local_binder_exprs], but does not take the [let] bindings into
     account. *)
+
+(** { 6 Folds and maps } *)
+
+(** Used in typeclasses *)
+val fold_constr_expr_with_binders : (Id.t -> 'a -> 'a) ->
+   ('a -> 'b -> constr_expr -> 'b) -> 'a -> 'b -> constr_expr -> 'b
+
+(** Used in correctness and interface; absence of var capture not guaranteed
+   in pattern-matching clauses and in binders of the form [x,y:T(x)] *)
+
+val map_constr_expr_with_binders :
+  (Id.t -> 'a -> 'a) -> ('a -> constr_expr -> constr_expr) ->
+      'a -> constr_expr -> constr_expr
+
+val replace_vars_constr_expr :
+  Id.t Id.Map.t -> constr_expr -> constr_expr
+
+(** Specific function for interning "in indtype" syntax of "match" *)
+val ids_of_cases_indtype : cases_pattern_expr -> Id.Set.t
+
+val free_vars_of_constr_expr : constr_expr -> Id.Set.t
+val occur_var_constr_expr : Id.t -> constr_expr -> bool
+
+val split_at_annot : local_binder_expr list -> Id.t located option -> local_binder_expr list * local_binder_expr list
+
+val ntn_loc : ?loc:Loc.t -> constr_notation_substitution -> string -> (int * int) list
+val patntn_loc : ?loc:Loc.t -> cases_pattern_notation_substitution -> string -> (int * int) list
+
+(** For cases pattern parsing errors *)
+val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a
+
+(** Placeholder for global option, should be moved to a parameter *)
+val asymmetric_patterns : bool ref