aboutsummaryrefslogtreecommitdiffhomepage
path: root/API
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-11-21 13:58:08 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-11-21 13:58:08 +0100
commitb75beb248873db7d9ab8e4a078022b2ed0edcd36 (patch)
tree4d2bc9d39c1f6d7c4d00223143f18ae5bad500e5 /API
parent0e01de69c22a3793855b4c97c50e4514191b19bc (diff)
parent094b577f61f105f0a92f3f84d7e739884dd993a7 (diff)
Merge PR #6185: [parser] Remove unnecessary statically initialized hook.
Diffstat (limited to 'API')
-rw-r--r--API/API.mli7
1 files changed, 6 insertions, 1 deletions
diff --git a/API/API.mli b/API/API.mli
index cc0de2b1b..51671fc3d 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 :