diff options
author | 2017-11-19 05:11:18 +0100 | |
---|---|---|
committer | 2017-11-19 17:42:48 +0100 | |
commit | 094b577f61f105f0a92f3f84d7e739884dd993a7 (patch) | |
tree | 33b39e64d139d2079734a84359707c2fa12451c3 /API | |
parent | edf1a8f36f75861b822081b3825357e122b6937d (diff) |
[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`.
Diffstat (limited to 'API')
-rw-r--r-- | API/API.mli | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/API/API.mli b/API/API.mli index 704f1a356..44d02ce2b 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 : |